diff --git a/packages/contracts-bedrock/.gitignore b/packages/contracts-bedrock/.gitignore index 96e09c8c7190..381d4fd80714 100644 --- a/packages/contracts-bedrock/.gitignore +++ b/packages/contracts-bedrock/.gitignore @@ -6,6 +6,7 @@ broadcast kout-deployment kout-proofs test/kontrol/logs +out/ # Metrics coverage.out @@ -40,3 +41,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 cef9f85bbaeb..4d120365d1b1 100644 --- a/packages/contracts-bedrock/foundry.toml +++ b/packages/contracts-bedrock/foundry.toml @@ -97,3 +97,15 @@ src = 'test/kontrol/proofs' out = 'kout-proofs' test = 'test/kontrol/proofs' script = 'test/kontrol/proofs' + +[profile.kontrol-properties] +src = "test/properties/kontrol" +test = "test/properties/kontrol" +script = "test/properties/kontrol" +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/kontrol.toml b/packages/contracts-bedrock/kontrol.toml new file mode 100644 index 000000000000..12da12c128b1 --- /dev/null +++ b/packages/contracts-bedrock/kontrol.toml @@ -0,0 +1,44 @@ +[build.default] +foundry-project-root = './' +regen = false +rekompile = false +verbose = false +debug = false +auxiliary-lemmas = true + +# require = 'lemmas.k' +# module-import = 'TestBase:KONTROL-LEMMAS' + +[prove.default] +foundry-project-root = './' +verbose = false +debug = false +max-depth = 25000 +reinit = false +cse = false +workers = 1 +failure-information = true +counterexample-information = true +minimize-proofs = false +fail-fast = true +smt-timeout = 1000 +break-every-step = false +break-on-jumpi = false +break-on-calls = false +break-on-storage = false +break-on-basic-blocks = false +break-on-cheatcodes = false +run-constructor = true +symbolic-immutables = false +schedule = 'CANCUN' +init-node-from-diff = 'supererc20-state-diff/StateDiff.json' + +[show.default] +foundry-project-root = '.' +verbose = false +debug = false +use-hex-encoding = false + +[view-kcfg.default] +foundry-project-root = '.' +use-hex-encoding = false 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..f87791116f3c --- /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": "0x610100604052348015610010575f80fd5b5060405161080038038061080083398101604081905261002f9161006d565b6001600160a01b039384166080529190921660a05260c09190915260e0526100ad565b80516001600160a01b0381168114610068575f80fd5b919050565b5f805f8060808587031215610080575f80fd5b61008985610052565b935061009760208601610052565b6040860151606090960151949790965092505050565b60805160a05160c05160e0516106ff6101015f395f818160a0015261020601525f818160e401526103e901525f818161039b015281816103c4015261041401525f8181610339015261036201526106ff5ff3fe608060405260043610610079575f3560e01c80637056f41f1161004c5780637056f41f1461013f578063722c2a4d1461015257806382dc9c8b146101ca578063f230b4c2146101f5575f80fd5b80631ecd26f21461007d57806324794462146100925780632ea02369146100d357806338ffde1814610106575b5f80fd5b61009061008b36600461059e565b610228565b005b34801561009d575f80fd5b507f00000000000000000000000000000000000000000000000000000000000000005b6040519081526020015b60405180910390f35b3480156100de575f80fd5b506100c07f000000000000000000000000000000000000000000000000000000000000000081565b348015610111575f80fd5b5061011a6102e3565b60405173ffffffffffffffffffffffffffffffffffffffff90911681526020016100ca565b61009061014d36600461061a565b6103e7565b34801561015d575f80fd5b5061009061016c366004610670565b5f805473ffffffffffffffffffffffffffffffffffffffff9092167fffffffffffffffffffffff0000000000000000000000000000000000000000009092169190911774010000000000000000000000000000000000000000179055565b3480156101d5575f80fd5b505f5461011a9073ffffffffffffffffffffffffffffffffffffffff1681565b348015610200575f80fd5b506100c07f000000000000000000000000000000000000000000000000000000000000000081565b5f808473ffffffffffffffffffffffffffffffffffffffff16348585604051610252929190610690565b5f6040518083038185875af1925050503d805f811461028c576040519150601f19603f3d011682016040523d82523d5f602084013e610291565b606091505b5091509150816102d857806040517f08c379a00000000000000000000000000000000000000000000000000000000081526004016102cf919061069f565b60405180910390fd5b505050505050505050565b5f805474010000000000000000000000000000000000000000900460ff161561032257505f5473ffffffffffffffffffffffffffffffffffffffff1690565b73ffffffffffffffffffffffffffffffffffffffff7f000000000000000000000000000000000000000000000000000000000000000016330361038457507f000000000000000000000000000000000000000000000000000000000000000090565b73ffffffffffffffffffffffffffffffffffffffff7f00000000000000000000000000000000000000000000000000000000000000001633036103e457507f00000000000000000000000000000000000000000000000000000000000000005b90565b7f00000000000000000000000000000000000000000000000000000000000000008403610500575f61046f7f00000000000000000000000000000000000000000000000000000000000000005f85858080601f0160208091040260200160405190810160405280939291908181526020018383808284375f9201919091525061050692505050565b9050806104fe576040517f08c379a000000000000000000000000000000000000000000000000000000000815260206004820152602760248201527f4d6f636b4c32546f4c324d657373656e6765723a2073656e644d65737361676560448201527f206661696c65640000000000000000000000000000000000000000000000000060648201526084016102cf565b505b50505050565b5f610513845a858561051b565b949350505050565b5f805f835160208501868989f195945050505050565b803573ffffffffffffffffffffffffffffffffffffffff81168114610554575f80fd5b919050565b5f8083601f840112610569575f80fd5b50813567ffffffffffffffff811115610580575f80fd5b602083019150836020828501011115610597575f80fd5b9250929050565b5f805f805f805f60c0888a0312156105b4575f80fd5b8735965060208801359550604088013594506105d260608901610531565b93506105e060808901610531565b925060a088013567ffffffffffffffff8111156105fb575f80fd5b6106078a828b01610559565b989b979a50959850939692959293505050565b5f805f806060858703121561062d575f80fd5b8435935061063d60208601610531565b9250604085013567ffffffffffffffff811115610658575f80fd5b61066487828801610559565b95989497509550505050565b5f60208284031215610680575f80fd5b61068982610531565b9392505050565b818382375f9101908152919050565b602081525f82518060208401528060208501604085015e5f6040828501015260407fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffe0601f8301168401019150509291505056fea164736f6c6343000819000a0000000000000000000000002e234dae75c793f67a35089c9d99245e1c58470b000000000000000000000000f62849f9a0b5bf2913b396098f7c7019b51a820a00000000000000000000000000000000000000000000000000000000000000020000000000000000000000000000000000000000000000000000000000000003", + "deployedCode": "0x608060405260043610610079575f3560e01c80637056f41f1161004c5780637056f41f1461013f578063722c2a4d1461015257806382dc9c8b146101ca578063f230b4c2146101f5575f80fd5b80631ecd26f21461007d57806324794462146100925780632ea02369146100d357806338ffde1814610106575b5f80fd5b61009061008b36600461059e565b610228565b005b34801561009d575f80fd5b507f00000000000000000000000000000000000000000000000000000000000000035b6040519081526020015b60405180910390f35b3480156100de575f80fd5b506100c07f000000000000000000000000000000000000000000000000000000000000000281565b348015610111575f80fd5b5061011a6102e3565b60405173ffffffffffffffffffffffffffffffffffffffff90911681526020016100ca565b61009061014d36600461061a565b6103e7565b34801561015d575f80fd5b5061009061016c366004610670565b5f805473ffffffffffffffffffffffffffffffffffffffff9092167fffffffffffffffffffffff0000000000000000000000000000000000000000009092169190911774010000000000000000000000000000000000000000179055565b3480156101d5575f80fd5b505f5461011a9073ffffffffffffffffffffffffffffffffffffffff1681565b348015610200575f80fd5b506100c07f000000000000000000000000000000000000000000000000000000000000000381565b5f808473ffffffffffffffffffffffffffffffffffffffff16348585604051610252929190610690565b5f6040518083038185875af1925050503d805f811461028c576040519150601f19603f3d011682016040523d82523d5f602084013e610291565b606091505b5091509150816102d857806040517f08c379a00000000000000000000000000000000000000000000000000000000081526004016102cf919061069f565b60405180910390fd5b505050505050505050565b5f805474010000000000000000000000000000000000000000900460ff161561032257505f5473ffffffffffffffffffffffffffffffffffffffff1690565b73ffffffffffffffffffffffffffffffffffffffff7f0000000000000000000000002e234dae75c793f67a35089c9d99245e1c58470b16330361038457507f0000000000000000000000002e234dae75c793f67a35089c9d99245e1c58470b90565b73ffffffffffffffffffffffffffffffffffffffff7f000000000000000000000000f62849f9a0b5bf2913b396098f7c7019b51a820a1633036103e457507f000000000000000000000000f62849f9a0b5bf2913b396098f7c7019b51a820a5b90565b7f00000000000000000000000000000000000000000000000000000000000000028403610500575f61046f7f000000000000000000000000f62849f9a0b5bf2913b396098f7c7019b51a820a5f85858080601f0160208091040260200160405190810160405280939291908181526020018383808284375f9201919091525061050692505050565b9050806104fe576040517f08c379a000000000000000000000000000000000000000000000000000000000815260206004820152602760248201527f4d6f636b4c32546f4c324d657373656e6765723a2073656e644d65737361676560448201527f206661696c65640000000000000000000000000000000000000000000000000060648201526084016102cf565b505b50505050565b5f610513845a858561051b565b949350505050565b5f805f835160208501868989f195945050505050565b803573ffffffffffffffffffffffffffffffffffffffff81168114610554575f80fd5b919050565b5f8083601f840112610569575f80fd5b50813567ffffffffffffffff811115610580575f80fd5b602083019150836020828501011115610597575f80fd5b9250929050565b5f805f805f805f60c0888a0312156105b4575f80fd5b8735965060208801359550604088013594506105d260608901610531565b93506105e060808901610531565b925060a088013567ffffffffffffffff8111156105fb575f80fd5b6106078a828b01610559565b989b979a50959850939692959293505050565b5f805f806060858703121561062d575f80fd5b8435935061063d60208601610531565b9250604085013567ffffffffffffffff811115610658575f80fd5b61066487828801610559565b95989497509550505050565b5f60208284031215610680575f80fd5b61068982610531565b9392505050565b818382375f9101908152919050565b602081525f82518060208401528060208501604085015e5f6040828501015260407fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffe0601f8301168401019150509291505056fea164736f6c6343000819000a", + "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/FoundryDebugSymbolic.t.sol b/packages/contracts-bedrock/test/properties/FoundryDebugSymbolic.t.sol new file mode 100644 index 000000000000..3ec067e25926 --- /dev/null +++ b/packages/contracts-bedrock/test/properties/FoundryDebugSymbolic.t.sol @@ -0,0 +1,123 @@ +// SPDX-License-Identifier: MIT +pragma solidity 0.8.25; + +import { OptimismSuperchainERC20 } from "src/L2/OptimismSuperchainERC20.sol"; +import { Predeploys } from "src/libraries/Predeploys.sol"; +import { MockL2ToL2Messenger } from "test/properties/kontrol/helpers/MockL2ToL2Messenger.sol"; +import { KontrolBase } from "test/properties/kontrol/KontrolBase.sol"; +import { ERC1967Proxy } from "@openzeppelin/contracts-v5/proxy/ERC1967/ERC1967Proxy.sol"; +import "forge-std/Test.sol"; + +// TODO: File to debug faster with foundry replicating scenarios where the proof failed, needs removal afterwards. +contract FoundryDebugTests is KontrolBase { + event CrossDomainMessageSender(address _sender); + + 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)) + ) + ) + ); + + mockL2ToL2Messenger = + new MockL2ToL2Messenger(address(sourceToken), address(destToken), DESTINATION_CHAIN_ID, SOURCE); + vm.etch(address(MESSENGER), address(mockL2ToL2Messenger).code); + } + + /// Check setup works as expected + function test_proveSetup() public { + // Source token + assert(remoteToken != address(0)); + assert(sourceToken.remoteToken() == remoteToken); + assert(eqStrings(sourceToken.name(), name)); + assert(eqStrings(sourceToken.symbol(), symbol)); + assert(sourceToken.decimals() == decimals); + vm.prank(address(sourceToken)); + assert(MESSENGER.crossDomainMessageSender() == address(sourceToken)); + + // Destination token + assert(destToken.remoteToken() == remoteToken); + assert(eqStrings(destToken.name(), name)); + assert(eqStrings(destToken.symbol(), symbol)); + assert(destToken.decimals() == decimals); + assert(MESSENGER.DESTINATION_CHAIN_ID() == DESTINATION_CHAIN_ID); + vm.prank(address(destToken)); + assert(MESSENGER.crossDomainMessageSender() == address(destToken)); + + // Custom cross domain sender + MESSENGER.forTest_setCustomCrossDomainSender(address(420)); + assert(MESSENGER.crossDomainMessageSender() == address(420)); + } + + // debug property-id 8 + // `sendERC20` with a value of zero does not modify accounting + function test_proveSendERC20ZeroCall() public { + /* Preconditions */ + address _from = address(511347974759188522659820409854212399244223280810); + address _to = address(376793390874373408599387495934666716005045108769); // 0x7Fa9385Be102aC3eac297483DD6233d62B3e1497 + uint256 _chainId = 0; + + uint256 _totalSupplyBefore = sourceToken.totalSupply(); + uint256 _fromBalanceBefore = sourceToken.balanceOf(_from); + uint256 _toBalanceBefore = sourceToken.balanceOf(_to); + + vm.startPrank(_from); + /* Action */ + sourceToken.sendERC20(_to, ZERO_AMOUNT, _chainId); + + /* Postcondition */ + assert(sourceToken.totalSupply() == _totalSupplyBefore); + assert(sourceToken.balanceOf(_from) == _fromBalanceBefore); + assert(sourceToken.balanceOf(_to) == _toBalanceBefore); + } + // ORIGIN_ID = 645326474426547203313410069153905908525362434350 + // CALLER_ID = 645326474426547203313410069153905908525362434350 + // NUMBER_CELL = 16777217 + // VV2__chainId_114b9705 = 0 + // VV0__from_114b9705 = 511347974759188522659820409854212399244223280810 + // TIMESTAMP_CELL = 1073741825 + // VV1__to_114b9705 = 376793390874373408599387495934666716005045108769 + + // debug 9 + // `relayERC20` with a value of zero does not modify accounting + function test_proveRelayERC20ZeroCall() public { + /* Preconditions */ + address _from = address(645326474426547203313410069153905908525362434350); + address _to = address(728815563385977040452943777879061427756277306519); + + uint256 _totalSupplyBefore = sourceToken.totalSupply(); + uint256 _fromBalanceBefore = sourceToken.balanceOf(_from); + uint256 _toBalanceBefore = sourceToken.balanceOf(_to); + + vm.prank(address(MESSENGER)); + /* Action */ + sourceToken.relayERC20(_from, _to, ZERO_AMOUNT); + + /* Postconditions */ + assert(sourceToken.totalSupply() == _totalSupplyBefore); + assert(sourceToken.balanceOf(_from) == _fromBalanceBefore); + assert(sourceToken.balanceOf(_to) == _toBalanceBefore); + } + // VV0__from_114b9705 = 645326474426547203313410069153905908525362434350 + // ORIGIN_ID = 645326474426547203313410069153905908525362434350 + // CALLER_ID = 645326474426547203313410069153905908525362434350 + // NUMBER_CELL = 16777217 + // VV1__to_114b9705 = 728815563385977040452943777879061427756277306519 + // TIMESTAMP_CELL = 1073741825 +} diff --git a/packages/contracts-bedrock/test/properties/PROPERTIES.md b/packages/contracts-bedrock/test/properties/PROPERTIES.md new file mode 100644 index 000000000000..748d9c306266 --- /dev/null +++ b/packages/contracts-bedrock/test/properties/PROPERTIES.md @@ -0,0 +1,126 @@ +# Supertoken advanced testing + +## Overview + +This document defines a set of properties global to the supertoken ecosystem, for which we will: + +- run a [Medusa](https://github.com/crytic/medusa) fuzzing campaign, trying to break system invariants +- formally prove with [Kontrol](https://docs.runtimeverification.com/kontrol) whenever possible + +## Milestones + +The supertoken ecosystem consists of not just the supertoken contract, but the required changes to other contracts for liquidity to reach the former. + +Considering only the supertoken contract is merged into the `develop` branch, and work for the other components is still in progress, we define three milestones for the testing campaign: + +- SupERC20: concerned with only the supertoken contract, the first one to be implemented +- Factories: covers the above + the development of `OptimismSuperchainERC20Factory` and required changes to `OptimismMintableERC20Factory` +- Liquidity Migration: includes the `convert` function on the `L2StandardBridgeInterop` to migrate liquidity from legacy tokens into supertokens + +## Where to place the testing campaign + +Given the [OP monorepo](https://github.com/ethereum-optimism/optimism) already has invariant testing provided by foundry, it's not a trivial matter where to place this advanced testing campaign. Two alternatives are proposed: + +- including it in the mainline OP monorepo, in a subdirectory of the existing test contracts such as `test/invariants/medusa/superc20/` +- keep the campaign in wonderland's fork of the repository, in its own feature branch, in which case the deliverable would consist primarily of: + - a summary of the results, extending this document + - PRs with extra unit tests replicating found issues to the main repo where applicable + +## Contracts in scope + +- [ ] [OptimismMintableERC20Factory](https://github.com/defi-wonderland/optimism/blob/develop/packages/contracts-bedrock/src/universal/OptimismMintableERC20Factory.sol) (modifications to enable `convert` not yet merged) +- [ ] [OptimismSuperchainERC20](https://github.com/defi-wonderland/optimism/blob/develop/packages/contracts-bedrock/src/L2/OptimismSuperchainERC20.sol1) +- [ ] [OptimismSuperchainERC20Factory](https://github.com/defi-wonderland/optimism/pull/8/files#diff-09838f5703c353d0f7c5ff395acc04c1768ef58becac67404bc17e1fb0018517) (not yet merged) +- [ ] [L2StandardBridgeInterop](https://github.com/defi-wonderland/optimism/pull/10/files#diff-56cf869412631eac0a04a03f7d026596f64a1e00fcffa713bc770d67c6856c2f) (not yet merged) + +## Behavior assumed correct + +- [ ] inclusion of relay transactions +- [ ] sequencer implementation +- [ ] [OptimismMintableERC20](https://github.com/defi-wonderland/optimism/blob/develop/packages/contracts-bedrock/src/universal/OptimismMintableERC20.sol) +- [ ] [L2ToL2CrossDomainMessenger](https://github.com/defi-wonderland/optimism/blob/develop/packages/contracts-bedrock/src/L2/L2CrossDomainMessenger.sol) +- [ ] [CrossL2Inbox](https://github.com/defi-wonderland/src/L2/CrossL2Inbox.sol) + +## Pain points + +- existing fuzzing tools use the same EVM to run the tested contracts as they do for asserting invariants, tracking ghost variables and everything else necessary to provision a fuzzing campaign. While this is usually very convenient, it means that we can’t assert on the behaviour/state of _different_ chains from within a fuzzing campaign. This means we will have to walk around the requirement of supertokens having the same address across all chains, and implement a way to mock tokens existing in different chains. We will strive to formally prove it in a unitary fashion to mitigate this in properties 0 and 1 +- a buffer to represent 'in transit' messages should be implemented to assert on invariants relating to the non-atomicity of bridging from one chain to another. It is yet to be determined if it’ll be a FIFO queue (assuming ideal message ordering by sequencers) or it’ll have random-access capability to simulate messages arriving out of order + +## Definitions + +- _legacy token:_ an OptimismMintableERC20 or L2StandardERC20 token on the suprechain that has either been deployed by the factory after the liquidity migration upgrade to the latter, or has been deployed before it **but** added to factory’s `deployments` mapping as part of the upgrade. This testing campaign is not concerned with tokens on L1 or not listed in the factory’s `deployments` mapping. +- _supertoken:_ a SuperchainERC20 contract deployed by the `OptimismSuperchainERC20Factory` + +# Ecosystem properties + +legend: + +- `[ ]`: property not yet tested +- `**[ ]**`: property not yet tested, dev/research team has asked for extra focus on it +- `[X]`: tested/proven property +- `[~]`: partially tested/proven property +- `:(`: property won't be tested due to some limitation + +## Unit test + +| id | milestone | description | kontrol | medusa | +| --- | ------------------- | ------------------------------------------------------------------------------------------ | ------- | ------ | +| 0 | Factories | supertoken token address does not depend on the executing chain’s chainID | [ ] | [ ] | +| 1 | Factories | supertoken token address depends on remote token, name, symbol and decimals | [ ] | [ ] | +| 2 | Liquidity Migration | convert() should only allow converting legacy tokens to supertoken and viceversa | [ ] | [ ] | +| 3 | Liquidity Migration | convert() only allows migrations between tokens representing the same remote asset | [ ] | [ ] | +| 4 | Liquidity Migration | convert() only allows migrations from tokens with the same decimals | [ ] | [ ] | +| 5 | Liquidity Migration | convert() burns the same amount of legacy token that it mints of supertoken, and viceversa | [ ] | [ ] | + +## Valid state + +| id | milestone | description | kontrol | medusa | +| --- | --------- | ------------------------------------------------------------------------------------------ | ------- | ------ | +| 6 | SupERC20 | calls to sendERC20 succeed as long as caller has enough balance | [x] | [ ] | +| 7 | SupERC20 | calls to relayERC20 always succeed as long as the sender and cross-domain caller are valid | **[x]** | [ ] | + +## Variable transition + +| id | milestone | description | kontrol | medusa | +| --- | ------------------- | ------------------------------------------------------------------------------------------------- | ------- | ------ | +| 8 | SupERC20 | sendERC20 with a value of zero does not modify accounting | [:(] | [ ] | +| 9 | SupERC20 | relayERC20 with a value of zero does not modify accounting | [:(] | [ ] | +| 10 | SupERC20 | sendERC20 decreases the token's totalSupply in the source chain exactly by the input amount | [x] | [ ] | +| 11 | SupERC20 | relayERC20 increases the token's totalSupply in the destination chain exactly by the input amount | [x] | [ ] | +| 12 | Liquidity Migration | supertoken total supply only increases on calls to mint() by the L2toL2StandardBridge | [x] | [~] | +| 13 | Liquidity Migration | supertoken total supply only decreases on calls to burn() by the L2toL2StandardBridge | [x] | [ ] | +| 14 | SupERC20 | supertoken total supply starts at zero | [x] | [x] | +| 15 | Factories | deploying a supertoken registers its remote token in the factory | [ ] | [ ] | +| 16 | Factories | deploying an OptimismMintableERC20 registers its remote token in the factory | [ ] | [ ] | + +## High level + +| id | milestone | description | kontrol | medusa | +| --- | ------------------- | --------------------------------------------------------------------------------------------------------------------------------------------------------------------- | ------- | ------ | +| 17 | Liquidity Migration | only calls to convert(legacy, super) can increase a supertoken’s total supply across chains | [ ] | [ ] | +| 18 | Liquidity Migration | only calls to convert(super, legacy) can decrease a supertoken’s total supply across chains | [ ] | [ ] | +| 19 | Liquidity Migration | sum of supertoken total supply across all chains is always <= to convert(legacy, super)- convert(super, legacy) | [ ] | [ ] | +| 20 | SupERC20 | tokens sendERC20-ed on a source chain to a destination chain can be relayERC20-ed on it as long as the source chain is in the dependency set of the destination chain | [ ] | [ ] | +| 21 | Liquidity Migration | sum of supertoken total supply across all chains is = to convert(legacy, super)- convert(super, legacy) when all cross-chain messages are processed | [ ] | [ ] | + +## Atomic bridging pseudo-properties + +As another layer of defense, the following properties are defined which assume bridging operations to be atomic (that is, the sequencer and L2Inbox and CrossDomainMessenger contracts are fully abstracted away, `sendERC20` triggering the `relayERC20` call on the same transaction) +It’s worth noting that these properties will not hold for a live system + +| id | milestone | description | kontrol | medusa | +| --- | ------------------- | ---------------------------------------------------------------------------------------------------------------------------------- | ------- | ------ | +| 22 | SupERC20 | sendERC20 decreases sender balance in source chain and increases receiver balance in destination chain exactly by the input amount | [ ] | [x] | +| 23 | SupERC20 | sendERC20 decreases total supply in source chain and increases it in destination chain exactly by the input amount | [ ] | [x] | +| 24 | Liquidity Migration | sum of supertoken total supply across all chains is always equal to convert(legacy, super)- convert(super, legacy) | [ ] | [~] | + +# Expected external interactions + +- regular ERC20 operations between any accounts on the same chain, provided by [crytic ERC20 properties](https://github.com/crytic/properties?tab=readme-ov-file#erc20-tests) + +# Invariant-breaking candidates (brain dump) + +here we’ll list possible interactions that we intend the fuzzing campaign to support in order to help break invariants + +- [ ] changing the decimals of tokens after deployment +- [ ] `convert()` ing between multiple (3+) representations of the same remote token, by having different names/symbols diff --git a/packages/contracts-bedrock/test/properties/helpers/MockL2ToL2CrossDomainMessenger.t.sol b/packages/contracts-bedrock/test/properties/helpers/MockL2ToL2CrossDomainMessenger.t.sol new file mode 100644 index 000000000000..0e3f819a6f06 --- /dev/null +++ b/packages/contracts-bedrock/test/properties/helpers/MockL2ToL2CrossDomainMessenger.t.sol @@ -0,0 +1,53 @@ +// SPDX-License-Identifier: MIT +pragma solidity ^0.8.25; + +import { OptimismSuperchainERC20 } from "src/L2/OptimismSuperchainERC20.sol"; +import { SafeCall } from "src/libraries/SafeCall.sol"; + +contract MockL2ToL2CrossDomainMessenger { + ///////////////////////////////////////////////////////// + // State vars mocking the L2toL2CrossDomainMessenger // + ///////////////////////////////////////////////////////// + address public crossDomainMessageSender; + address public crossDomainMessageSource; + + /////////////////////////////////////////////////// + // Helpers for cross-chain interaction mocking // + /////////////////////////////////////////////////// + mapping(address supertoken => bytes32 deploySalt) public superTokenInitDeploySalts; + mapping(uint256 chainId => mapping(bytes32 deploySalt => address supertoken)) public superTokenAddresses; + + function crossChainMessageReceiver( + address sender, + uint256 destinationChainId + ) + external + view + returns (OptimismSuperchainERC20) + { + return OptimismSuperchainERC20(superTokenAddresses[destinationChainId][superTokenInitDeploySalts[sender]]); + } + + function registerSupertoken(bytes32 deploySalt, uint256 chainId, address token) external { + superTokenAddresses[chainId][deploySalt] = token; + superTokenInitDeploySalts[token] = deploySalt; + } + + //////////////////////////////////////////////////////// + // Functions mocking the L2toL2CrossDomainMessenger // + //////////////////////////////////////////////////////// + + /// @notice recipient will not be used since in normal execution it's the same + /// address on a different chain, but here we have to compute it to mock + /// cross-chain messaging + function sendMessage(uint256 chainId, address, /*recipient*/ bytes memory message) external { + address crossChainRecipient = superTokenAddresses[chainId][superTokenInitDeploySalts[msg.sender]]; + if (crossChainRecipient == msg.sender) { + require(false, "same chain"); + } + crossDomainMessageSender = crossChainRecipient; + crossDomainMessageSource = msg.sender; + SafeCall.call(crossDomainMessageSender, 0, message); + crossDomainMessageSender = address(0); + } +} 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..467b8c225540 --- /dev/null +++ b/packages/contracts-bedrock/test/properties/kontrol/KontrolBase.sol @@ -0,0 +1,66 @@ +// 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/kontrol/helpers/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 SOURCE = 3; + 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, SOURCE); + + 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/OptimismSuperchainERC20.k.sol b/packages/contracts-bedrock/test/properties/kontrol/OptimismSuperchainERC20.k.sol new file mode 100644 index 000000000000..854ea6353af1 --- /dev/null +++ b/packages/contracts-bedrock/test/properties/kontrol/OptimismSuperchainERC20.k.sol @@ -0,0 +1,329 @@ +// SPDX-License-Identifier: MIT +pragma solidity 0.8.25; + +import { OptimismSuperchainERC20 } from "src/L2/OptimismSuperchainERC20.sol"; +import { Predeploys } from "src/libraries/Predeploys.sol"; +import { MockL2ToL2Messenger } from "test/properties/kontrol/helpers/MockL2ToL2Messenger.sol"; +import { KontrolBase } from "test/properties/kontrol/KontrolBase.sol"; +import { InitialState } from "./deployments/InitialState.sol"; + +contract OptimismSuperchainERC20Kontrol is KontrolBase, InitialState { + event CrossDomainMessageSender(address _sender); + + /// @notice Use this function instead of `setUp()` for performance reasons when running the proofs with Kontrol + 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)); + assert(eqStrings(sourceToken.symbol(), symbol)); + assert(sourceToken.decimals() == decimals); + vm.prank(address(sourceToken)); + assert(MESSENGER.crossDomainMessageSender() == address(sourceToken)); + + // Destination token + assert(destToken.remoteToken() == remoteToken); + assert(eqStrings(destToken.name(), name)); + assert(eqStrings(destToken.symbol(), symbol)); + assert(destToken.decimals() == decimals); + assert(MESSENGER.DESTINATION_CHAIN_ID() == DESTINATION_CHAIN_ID); + vm.prank(address(destToken)); + assert(MESSENGER.crossDomainMessageSender() == address(destToken)); + + // Messenger + assert(MESSENGER.SOURCE() == SOURCE); + assert(MESSENGER.crossDomainMessageSender() == address(0)); + // Check the setter works properly + MESSENGER.forTest_setCustomCrossDomainSender(address(420)); + assert(MESSENGER.crossDomainMessageSender() == address(420)); + } + + /// @custom:property-id 6 + /// @custom:property Calls to sendERC20 succeed as long as caller has enough balance + function prove_sendERC20SucceedsOnlyIfEnoughBalance( + uint256 _initialBalance, + address _from, + uint256 _amount, + address _to, + uint256 _chainId + ) + public + { + setUpInlined(); + + /* Preconditions */ + vm.assume(_to != address(0)); + vm.assume(_from != address(0)); + + vm.assume(notBuiltinAddress(_from)); + vm.assume(notBuiltinAddress(_to)); + + // Mint the amount to the caller + vm.prank(Predeploys.L2_STANDARD_BRIDGE); + sourceToken.mint(_from, _initialBalance); + + vm.prank(_from); + /* Action */ + try sourceToken.sendERC20(_to, _amount, _chainId) { + /* Postcondition */ + assert(_initialBalance >= _amount); + } catch { + assert(_initialBalance < _amount); + } + } + + /// @custom:property-id 7 + /// @custom:property Calls to relayERC20 always succeed as long as the sender and the cross-domain caller are valid + function prove_relayERC20OnlyFromL2ToL2Messenger( + address _crossDomainSender, + address _sender, + address _from, + address _to, + uint256 _amount + ) + public + { + setUpInlined(); + + /* Preconditions */ + vm.assume(_to != address(0)); + vm.assume(notBuiltinAddress(_from)); + vm.assume(notBuiltinAddress(_to)); + vm.assume(notBuiltinAddress(_sender)); + + MESSENGER.forTest_setCustomCrossDomainSender(_crossDomainSender); + + vm.prank(_sender); + /* Action */ + try sourceToken.relayERC20(_from, _to, _amount) { + /* Postconditions */ + assert(_sender == address(MESSENGER)); + assert(_crossDomainSender == address(sourceToken)); + } catch { + // Emit to bypass the check when the call fails + emit CrossDomainMessageSender(_crossDomainSender); + assert(_sender != address(MESSENGER) || _crossDomainSender != address(sourceToken)); + } + } + + /// @custom:property-id 8 + /// @custom:property `sendERC20` with a value of zero does not modify accounting + /// @custom:property-not-tested The proof fails - probably needs some fixes through lemmas and node pruning + function prove_sendERC20ZeroCall(address _from, address _to, uint256 _chainId) public { + setUpInlined(); + + /* Preconditions */ + vm.assume(_to != address(0)); + vm.assume(_to != address(Predeploys.CROSS_L2_INBOX)); + vm.assume(_to != address(MESSENGER)); + + vm.assume(notBuiltinAddress(_from)); + vm.assume(notBuiltinAddress(_to)); + + uint256 _totalSupplyBefore = sourceToken.totalSupply(); + uint256 _fromBalanceBefore = sourceToken.balanceOf(_from); + uint256 _toBalanceBefore = sourceToken.balanceOf(_to); + + vm.startPrank(_from); + /* Action */ + sourceToken.sendERC20(_to, ZERO_AMOUNT, _chainId); + + /* Postcondition */ + assert(sourceToken.totalSupply() == _totalSupplyBefore); + assert(sourceToken.balanceOf(_from) == _fromBalanceBefore); + assert(sourceToken.balanceOf(_to) == _toBalanceBefore); + } + + /// @custom:property-id 9 + /// @custom:property `relayERC20` with a value of zero does not modify accounting + /// @custom:property-not-tested The proof fails - probably needs some fixes through lemmas and node pruning + function prove_relayERC20ZeroCall(address _from, address _to) public { + setUpInlined(); + + /* Preconditions */ + vm.assume(_to != address(0)); + vm.assume(notBuiltinAddress(_from)); + vm.assume(notBuiltinAddress(_to)); + + uint256 _totalSupplyBefore = sourceToken.totalSupply(); + uint256 _fromBalanceBefore = sourceToken.balanceOf(_from); + uint256 _toBalanceBefore = sourceToken.balanceOf(_to); + + vm.prank(address(MESSENGER)); + /* Action */ + sourceToken.relayERC20(_from, _to, ZERO_AMOUNT); + + /* Postconditions */ + assert(sourceToken.totalSupply() == _totalSupplyBefore); + assert(sourceToken.balanceOf(_from) == _fromBalanceBefore); + assert(sourceToken.balanceOf(_to) == _toBalanceBefore); + } + + /// @custom:property-id 10 + /// @custom:property `sendERC20` decreases the token's totalSupply in the source chain exactly by the input amount + function prove_sendERC20DecreasesTotalSupply( + address _sender, + address _to, + uint256 _amount, + uint256 _chainId + ) + public + { + setUpInlined(); + + /* Preconditions */ + vm.assume(notBuiltinAddress(_sender)); + vm.assume(notBuiltinAddress(_to)); + + vm.assume(_sender != address(0)); + vm.assume(_to != address(0)); + + vm.prank(Predeploys.L2_STANDARD_BRIDGE); + sourceToken.mint(_sender, _amount); + + uint256 _totalSupplyBefore = sourceToken.totalSupply(); + uint256 _balanceBefore = sourceToken.balanceOf(_sender); + + vm.prank(_sender); + /* Action */ + sourceToken.sendERC20(Predeploys.CROSS_L2_INBOX, _amount, _chainId); + + /* Postconditions */ + assert(sourceToken.totalSupply() == _totalSupplyBefore - _amount); + assert(sourceToken.balanceOf(_sender) == _balanceBefore - _amount); + } + + /// @custom:property-id 11 + /// @custom:property `relayERC20` increases the token's totalSupply in the destination chain exactly by the input + /// amount + function prove_relayERC20IncreasesTotalSupply(address _from, address _to, uint256 _amount) public { + setUpInlined(); + + /* Preconditions */ + vm.assume(_to != address(0)); + vm.assume(notBuiltinAddress(_from)); + vm.assume(notBuiltinAddress(_to)); + + uint256 _totalSupplyBefore = sourceToken.totalSupply(); + uint256 _toBalanceBefore = sourceToken.balanceOf(_to); + + vm.prank(address(MESSENGER)); + /* Action */ + sourceToken.relayERC20(_from, _to, _amount); + + /* Postconditions */ + assert(sourceToken.totalSupply() == _totalSupplyBefore + _amount); + assert(sourceToken.balanceOf(_to) == _toBalanceBefore + _amount); + } + + /// @custom:property-id 12 + /// @custom:property Increases the total supply on the amount minted by the bridge + function prove_mint(address _from, uint256 _amount) public { + setUpInlined(); + + /* Preconditions */ + vm.assume(_from != address(0)); + vm.assume(notBuiltinAddress(_from)); + + uint256 _totalSupplyBefore = sourceToken.totalSupply(); + uint256 _balanceBefore = sourceToken.balanceOf(_from); + + vm.startPrank(Predeploys.L2_STANDARD_BRIDGE); + /* Action */ + sourceToken.mint(_from, _amount); + + /* Postconditions */ + assert(sourceToken.totalSupply() == _totalSupplyBefore + _amount); + assert(sourceToken.balanceOf(_from) == _balanceBefore + _amount); + } + + /// @custom:property-id 13 + /// @custom:property Supertoken total supply only decreases on the amount burned by the bridge + function prove_burn(address _from, uint256 _amount) public { + setUpInlined(); + + /* Preconditions */ + vm.assume(_from != address(0)); + vm.assume(notBuiltinAddress(_from)); + + vm.prank(Predeploys.L2_STANDARD_BRIDGE); + sourceToken.mint(_from, _amount); + + uint256 _totalSupplyBefore = sourceToken.totalSupply(); + uint256 _balanceBefore = sourceToken.balanceOf(_from); + + vm.prank(Predeploys.L2_STANDARD_BRIDGE); + /* Action */ + sourceToken.burn(_from, _amount); + + /* Postconditions */ + assert(sourceToken.totalSupply() == _totalSupplyBefore - _amount); + assert(sourceToken.balanceOf(_from) == _balanceBefore - _amount); + } + + /// @custom:property-id 14 + /// @custom:property Supertoken total supply starts at zero + function prove_totalSupplyStartsAtZero() public { + setUpInlined(); + + /* Postconditions */ + assert(sourceToken.totalSupply() == 0); + } + + /// @custom:property-id 22 + /// @custom:property `sendERC20` decreases sender balance in source chain and increases receiver balance in + /// destination chain exactly by the input amount + /// @custom:property-id 23 + /// @custom:property `sendERC20` decreases total supply in source chain and increases it in destination chain + /// exactly by the input amount + function prove_crossChainSendERC20(address _from, address _to, uint256 _amount, uint256 _chainId) public { + setUpInlined(); + + vm.assume(notBuiltinAddress(_from)); + vm.assume(notBuiltinAddress(_to)); + + /* Preconditions */ + vm.assume(_to != address(0)); + vm.assume(_from != address(0)); + + vm.prank(Predeploys.L2_STANDARD_BRIDGE); + sourceToken.mint(_from, _amount); + + uint256 fromBalanceBefore = sourceToken.balanceOf(_from); + uint256 toBalanceBefore = destToken.balanceOf(_to); + uint256 sourceTotalSupplyBefore = sourceToken.totalSupply(); + uint256 destTotalSupplyBefore = destToken.totalSupply(); + + vm.prank(_from); + /* Action */ + try sourceToken.sendERC20(_to, _amount, _chainId) { + /* Postconditions */ + // Source + assert(sourceToken.balanceOf(_from) == fromBalanceBefore - _amount); + assert(sourceToken.totalSupply() == sourceTotalSupplyBefore - _amount); + + // Destination + if (_chainId == DESTINATION_CHAIN_ID) { + // If the destination chain matches the one of the dest token, check that the amount was minted + assert(destToken.balanceOf(_to) == toBalanceBefore + _amount); + assert(destToken.totalSupply() == destTotalSupplyBefore + _amount); + } else { + // Otherwise the balances should remain the same + assert(destToken.balanceOf(_to) == toBalanceBefore); + assert(destToken.totalSupply() == destTotalSupplyBefore); + } + } catch { + // Shouldn't fail + assert(false); + } + } +} 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..fa587471be8b --- /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"608060405260043610610079575f3560e01c80637056f41f1161004c5780637056f41f1461013f578063722c2a4d1461015257806382dc9c8b146101ca578063f230b4c2146101f5575f80fd5b80631ecd26f21461007d57806324794462146100925780632ea02369146100d357806338ffde1814610106575b5f80fd5b61009061008b36600461059e565b610228565b005b34801561009d575f80fd5b507f00000000000000000000000000000000000000000000000000000000000000035b6040519081526020015b60405180910390f35b3480156100de575f80fd5b506100c07f000000000000000000000000000000000000000000000000000000000000000281565b348015610111575f80fd5b5061011a6102e3565b60405173ffffffffffffffffffffffffffffffffffffffff90911681526020016100ca565b61009061014d36600461061a565b6103e7565b34801561015d575f80fd5b5061009061016c366004610670565b5f805473ffffffffffffffffffffffffffffffffffffffff9092167fffffffffffffffffffffff0000000000000000000000000000000000000000009092169190911774010000000000000000000000000000000000000000179055565b3480156101d5575f80fd5b505f5461011a9073ffffffffffffffffffffffffffffffffffffffff1681565b348015610200575f80fd5b506100c07f000000000000000000000000000000000000000000000000000000000000000381565b5f808473ffffffffffffffffffffffffffffffffffffffff16348585604051610252929190610690565b5f6040518083038185875af1925050503d805f811461028c576040519150601f19603f3d011682016040523d82523d5f602084013e610291565b606091505b5091509150816102d857806040517f08c379a00000000000000000000000000000000000000000000000000000000081526004016102cf919061069f565b60405180910390fd5b505050505050505050565b5f805474010000000000000000000000000000000000000000900460ff161561032257505f5473ffffffffffffffffffffffffffffffffffffffff1690565b73ffffffffffffffffffffffffffffffffffffffff7f0000000000000000000000002e234dae75c793f67a35089c9d99245e1c58470b16330361038457507f0000000000000000000000002e234dae75c793f67a35089c9d99245e1c58470b90565b73ffffffffffffffffffffffffffffffffffffffff7f000000000000000000000000f62849f9a0b5bf2913b396098f7c7019b51a820a1633036103e457507f000000000000000000000000f62849f9a0b5bf2913b396098f7c7019b51a820a5b90565b7f00000000000000000000000000000000000000000000000000000000000000028403610500575f61046f7f000000000000000000000000f62849f9a0b5bf2913b396098f7c7019b51a820a5f85858080601f0160208091040260200160405190810160405280939291908181526020018383808284375f9201919091525061050692505050565b9050806104fe576040517f08c379a000000000000000000000000000000000000000000000000000000000815260206004820152602760248201527f4d6f636b4c32546f4c324d657373656e6765723a2073656e644d65737361676560448201527f206661696c65640000000000000000000000000000000000000000000000000060648201526084016102cf565b505b50505050565b5f610513845a858561051b565b949350505050565b5f805f835160208501868989f195945050505050565b803573ffffffffffffffffffffffffffffffffffffffff81168114610554575f80fd5b919050565b5f8083601f840112610569575f80fd5b50813567ffffffffffffffff811115610580575f80fd5b602083019150836020828501011115610597575f80fd5b9250929050565b5f805f805f805f60c0888a0312156105b4575f80fd5b8735965060208801359550604088013594506105d260608901610531565b93506105e060808901610531565b925060a088013567ffffffffffffffff8111156105fb575f80fd5b6106078a828b01610559565b989b979a50959850939692959293505050565b5f805f806060858703121561062d575f80fd5b8435935061063d60208601610531565b9250604085013567ffffffffffffffff811115610658575f80fd5b61066487828801610559565b95989497509550505050565b5f60208284031215610680575f80fd5b61068982610531565b9392505050565b818382375f9101908152919050565b602081525f82518060208401528060208501604085015e5f6040828501015260407fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffe0601f8301168401019150509291505056fea164736f6c6343000819000a"; +} 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/MockL2ToL2Messenger.sol b/packages/contracts-bedrock/test/properties/kontrol/helpers/MockL2ToL2Messenger.sol new file mode 100644 index 000000000000..82a6ce20c768 --- /dev/null +++ b/packages/contracts-bedrock/test/properties/kontrol/helpers/MockL2ToL2Messenger.sol @@ -0,0 +1,70 @@ +// SPDX-License-Identifier: MIT +pragma solidity 0.8.25; + +import "src/L2/L2ToL2CrossDomainMessenger.sol"; +import { SafeCall } from "src/libraries/SafeCall.sol"; + +// Mock contract for the L2ToL2Messenger contract where cross chain atomicity is simulated +contract MockL2ToL2Messenger { + event CrossDomainMessageSender(address _sender); + + address internal immutable SOURCE_TOKEN; + address internal immutable DESTINATION_TOKEN; + uint256 public immutable DESTINATION_CHAIN_ID; + uint256 public immutable SOURCE; + + // Custom cross domain sender to be used when neither the source nor destination token are the callers + address public customCrossDomainSender; + bool internal crossDomainSenderSet; + + constructor(address _sourceToken, address _destinationToken, uint256 _destinationChainId, uint256 _source) { + SOURCE_TOKEN = _sourceToken; + DESTINATION_TOKEN = _destinationToken; + DESTINATION_CHAIN_ID = _destinationChainId; + SOURCE = _source; + } + + // Mock the sendMessage function to execute the message call and simulate an atomic environmanet if the destination + // chain id matches the defined one + function sendMessage(uint256 _destination, address, bytes calldata _message) external payable { + // Mocking the environment to allow atomicity by executing the message call + if (_destination == DESTINATION_CHAIN_ID) { + (bool _success) = SafeCall.call(DESTINATION_TOKEN, 0, _message); + if (!_success) revert("MockL2ToL2Messenger: sendMessage failed"); + } + } + + // Mock the relay message function to just call the target address with the input message + function relayMessage( + uint256, + uint256, + uint256, + address, + address _target, + bytes calldata _message + ) + external + payable + { + (bool succ, bytes memory ret) = _target.call{ value: msg.value }(_message); + if (!succ) revert(string(ret)); + } + + function crossDomainMessageSource() external view returns (uint256 _source) { + _source = SOURCE; + } + + // Mock this function so it defaults to the custom domain sender if set, otherwise it defaults to the address of the + // token that called the function - reverts if neither are met + function crossDomainMessageSender() external view returns (address _sender) { + if (crossDomainSenderSet) _sender = customCrossDomainSender; + else if (msg.sender == SOURCE_TOKEN) _sender = SOURCE_TOKEN; + else if (msg.sender == DESTINATION_TOKEN) _sender = DESTINATION_TOKEN; + } + + /// Setter function for the customCrossDomainSender + function forTest_setCustomCrossDomainSender(address _customCrossDomainSender) external { + crossDomainSenderSet = true; + customCrossDomainSender = _customCrossDomainSender; + } +} 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..5251d4b4d70b --- /dev/null +++ b/packages/contracts-bedrock/test/properties/kontrol/helpers/RecordStateDiff.sol @@ -0,0 +1,78 @@ +// This code was originally copied from: +// https://github.com/runtimeverification/kontrol/blob/86451cbdaef8bed0370bf804fa4b545ec8b7a28a/docs/external-computation/test/kontrol/state-diff/record-state-diff/RecordStateDiff.sol +// It has been slightly modified, including changes to the compiler version. +// 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/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