diff --git a/.gitignore b/.gitignore index a2067e7d..ba68ab76 100644 --- a/.gitignore +++ b/.gitignore @@ -13,3 +13,4 @@ lib /broadcast lcov.info lcov_filtered.info +emv-* diff --git a/certora/applyHarness.patch b/certora/applyHarness.patch index 7313fa0d..034e081f 100644 --- a/certora/applyHarness.patch +++ b/certora/applyHarness.patch @@ -1,6 +1,6 @@ diff -ruN ../src/contracts/atlas/Atlas.sol contracts/atlas/Atlas.sol ---- ../src/contracts/atlas/Atlas.sol 2024-11-26 17:59:53.000000000 +0530 -+++ contracts/atlas/Atlas.sol 2024-12-02 23:21:50.000000000 +0530 +--- ../src/contracts/atlas/Atlas.sol 2024-12-21 01:46:37 ++++ contracts/atlas/Atlas.sol 2024-12-21 01:51:56 @@ -98,30 +98,34 @@ // userOpHash has already been calculated and verified in validateCalls at this point, so rather // than re-calculate it, we can simply take it from the dAppOp here. It's worth noting that this will @@ -10,7 +10,15 @@ diff -ruN ../src/contracts/atlas/Atlas.sol contracts/atlas/Atlas.sol - // Gas Refund to sender only if execution is successful - (uint256 _ethPaidToBundler, uint256 _netGasSurcharge) = - _settle(ctx, _dConfig.solverGasLimit, gasRefundBeneficiary); -- ++ // start of munging ++ Context memory ctx = this.execute(_dConfig, userOp, solverOps, _executionEnvironment, _bundler, dAppOp.userOpHash, _isSimulation); ++ _settle(ctx, _dConfig.solverGasLimit, gasRefundBeneficiary); ++ // try this.execute(_dConfig, userOp, solverOps, _executionEnvironment, _bundler, dAppOp.userOpHash, _isSimulation) ++ // returns (Context memory ctx) { ++ // // Gas Refund to sender only if execution is successful ++ // (uint256 _ethPaidToBundler, uint256 _netGasSurcharge) = ++ // _settle(ctx, _dConfig.solverGasLimit, gasRefundBeneficiary); + - auctionWon = ctx.solverSuccessful; - emit MetacallResult( - msg.sender, userOp.from, auctionWon, ctx.paymentsSuccessful, _ethPaidToBundler, _netGasSurcharge @@ -20,24 +28,6 @@ diff -ruN ../src/contracts/atlas/Atlas.sol contracts/atlas/Atlas.sol - _handleErrors(revertData, _dConfig.callConfig); - // Set lock to FullyLocked to prevent any reentrancy possibility - _setLockPhase(uint8(ExecutionPhase.FullyLocked)); -- -- // Refund the msg.value to sender if it errored -- // WARNING: If msg.sender is a disposable address such as a session key, make sure to remove ETH from it -- // before disposal -- if (msg.value != 0) SafeTransferLib.safeTransferETH(msg.sender, msg.value); -- -- // Emit event indicating the metacall failed in `execute()` -- emit MetacallResult(msg.sender, userOp.from, false, false, 0, 0); -- } -+ // start of munging -+ Context memory ctx = this.execute(_dConfig, userOp, solverOps, _executionEnvironment, _bundler, dAppOp.userOpHash, _isSimulation); -+ _settle(ctx, _dConfig.solverGasLimit, gasRefundBeneficiary); -+ // try this.execute(_dConfig, userOp, solverOps, _executionEnvironment, _bundler, dAppOp.userOpHash, _isSimulation) -+ // returns (Context memory ctx) { -+ // // Gas Refund to sender only if execution is successful -+ // (uint256 _ethPaidToBundler, uint256 _netGasSurcharge) = -+ // _settle(ctx, _dConfig.solverGasLimit, gasRefundBeneficiary); -+ + // auctionWon = ctx.solverSuccessful; + // emit MetacallResult( + // msg.sender, userOp.from, auctionWon, ctx.paymentsSuccessful, _ethPaidToBundler, _netGasSurcharge @@ -47,12 +37,19 @@ diff -ruN ../src/contracts/atlas/Atlas.sol contracts/atlas/Atlas.sol + // _handleErrors(revertData, _dConfig.callConfig); + // // Set lock to FullyLocked to prevent any reentrancy possibility + // _setLockPhase(uint8(ExecutionPhase.FullyLocked)); -+ + +- // Refund the msg.value to sender if it errored +- // WARNING: If msg.sender is a disposable address such as a session key, make sure to remove ETH from it +- // before disposal +- if (msg.value != 0) SafeTransferLib.safeTransferETH(msg.sender, msg.value); + // // Refund the msg.value to sender if it errored + // // WARNING: If msg.sender is a disposable address such as a session key, make sure to remove ETH from it + // // before disposal + // if (msg.value != 0) SafeTransferLib.safeTransferETH(msg.sender, msg.value); -+ + +- // Emit event indicating the metacall failed in `execute()` +- emit MetacallResult(msg.sender, userOp.from, false, false, 0, 0); +- } + // // Emit event indicating the metacall failed in `execute()` + // emit MetacallResult(msg.sender, userOp.from, false, false, 0, 0); + // } @@ -60,18 +57,9 @@ diff -ruN ../src/contracts/atlas/Atlas.sol contracts/atlas/Atlas.sol // The environment lock is explicitly released here to allow multiple metacalls in a single transaction. _releaseLock(); -@@ -162,7 +166,7 @@ - } - - // UserOp Call -- _returnData = _executeUserOperation(ctx, dConfig, userOp, _returnData); -+ // _returnData = _executeUserOperation(ctx, dConfig, userOp, _returnData); - - // SolverOps Calls - uint256 _winningBidAmount = dConfig.callConfig.exPostBids() diff -ruN ../src/contracts/atlas/AtlasVerification.sol contracts/atlas/AtlasVerification.sol ---- ../src/contracts/atlas/AtlasVerification.sol 2024-11-29 02:55:44.000000000 +0530 -+++ contracts/atlas/AtlasVerification.sol 2024-12-09 20:12:23.000000000 +0530 +--- ../src/contracts/atlas/AtlasVerification.sol 2024-12-21 01:46:37 ++++ contracts/atlas/AtlasVerification.sol 2024-12-21 01:46:37 @@ -50,110 +50,110 @@ external returns (ValidCallsResult) @@ -79,25 +67,42 @@ diff -ruN ../src/contracts/atlas/AtlasVerification.sol contracts/atlas/AtlasVeri - if (msg.sender != ATLAS) revert AtlasErrors.InvalidCaller(); - // Verify that the calldata injection came from the dApp frontend - // and that the signatures are valid. -- ++ // if (msg.sender != ATLAS) revert AtlasErrors.InvalidCaller(); ++ // // Verify that the calldata injection came from the dApp frontend ++ // // and that the signatures are valid. + - bytes32 _userOpHash = _getUserOperationHash(userOp, userOp.callConfig.allowsTrustedOpHash()); -- ++ // bytes32 _userOpHash = _getUserOperationHash(userOp, userOp.callConfig.allowsTrustedOpHash()); + - { - // Check user signature - ValidCallsResult verifyUserResult = _verifyUser(dConfig, userOp, _userOpHash, msgSender, isSimulation); - if (verifyUserResult != ValidCallsResult.Valid) { - return verifyUserResult; - } -- ++ // { ++ // // Check user signature ++ // ValidCallsResult verifyUserResult = _verifyUser(dConfig, userOp, _userOpHash, msgSender, isSimulation); ++ // if (verifyUserResult != ValidCallsResult.Valid) { ++ // return verifyUserResult; ++ // } + - // allowUnapprovedDAppSignatories still verifies signature match, but does not check - // if dApp owner approved the signer. - (ValidCallsResult verifyAuctioneerResult, bool allowUnapprovedDAppSignatories) = - _verifyAuctioneer(dConfig, userOp, solverOps, dAppOp, msgSender); -- ++ // // allowUnapprovedDAppSignatories still verifies signature match, but does not check ++ // // if dApp owner approved the signer. ++ // (ValidCallsResult verifyAuctioneerResult, bool allowUnapprovedDAppSignatories) = ++ // _verifyAuctioneer(dConfig, userOp, solverOps, dAppOp, msgSender); + - if (verifyAuctioneerResult != ValidCallsResult.Valid && !isSimulation) { - return verifyAuctioneerResult; - } -- ++ // if (verifyAuctioneerResult != ValidCallsResult.Valid && !isSimulation) { ++ // return verifyAuctioneerResult; ++ // } + - // Check dapp signature - ValidCallsResult verifyDappResult = - _verifyDApp(dConfig, dAppOp, msgSender, allowUnapprovedDAppSignatories, isSimulation); @@ -105,103 +110,6 @@ diff -ruN ../src/contracts/atlas/AtlasVerification.sol contracts/atlas/AtlasVeri - return verifyDappResult; - } - } -- -- // Check if the call configuration is valid -- ValidCallsResult _verifyCallConfigResult = _verifyCallConfig(dConfig.callConfig); -- if (_verifyCallConfigResult != ValidCallsResult.Valid) { -- return _verifyCallConfigResult; -- } -- -- // CASE: Solvers trust app to update content of UserOp after submission of solverOp -- if (dConfig.callConfig.allowsTrustedOpHash()) { -- // SessionKey must match explicitly - cannot be skipped -- if (userOp.sessionKey != dAppOp.from && !isSimulation) { -- return ValidCallsResult.InvalidAuctioneer; -- } -- -- // msgSender (the bundler) must be userOp.from, userOp.sessionKey / dappOp.from, or dappOp.bundler -- if (!(msgSender == dAppOp.from || msgSender == dAppOp.bundler || msgSender == userOp.from) && !isSimulation) -- { -- return ValidCallsResult.InvalidBundler; -- } -- } -- -- uint256 _solverOpCount = solverOps.length; -- -- { -- // Check number of solvers not greater than max, to prevent overflows in `solverIndex` -- if (_solverOpCount > _MAX_SOLVERS) { -- return ValidCallsResult.TooManySolverOps; -- } -- -- // Check if past user's deadline -- if (userOp.deadline != 0 && block.number > userOp.deadline) { -- return ValidCallsResult.UserDeadlineReached; -- } -- -- // Check if past dapp's deadline -- if (dAppOp.deadline != 0 && block.number > dAppOp.deadline) { -- return ValidCallsResult.DAppDeadlineReached; -- } -- -- // Check gas price is within user's limit -- if (tx.gasprice > userOp.maxFeePerGas) { -- return ValidCallsResult.GasPriceHigherThanMax; -- } -- -- // Check that the value of the tx is greater than or equal to the value specified -- if (msgValue < userOp.value) { -- return ValidCallsResult.TxValueLowerThanCallValue; -- } -- -- // Check the call config read at the start of the metacall is same as user expected (as set in userOp) -- if (dConfig.callConfig != userOp.callConfig) { -- return ValidCallsResult.CallConfigMismatch; -- } -- } -- -- // Some checks are only needed when call is not a simulation -- if (isSimulation) { -- // Add all solver ops if simulation -- return ValidCallsResult.Valid; -- } -- -- // Verify a solver was successfully verified. -- if (_solverOpCount == 0) { -- if (!dConfig.callConfig.allowsZeroSolvers()) { -- return ValidCallsResult.NoSolverOp; -- } -- -- if (dConfig.callConfig.needsFulfillment()) { -- return ValidCallsResult.NoSolverOp; -- } -- } -- -- if (_userOpHash != dAppOp.userOpHash) { -- return ValidCallsResult.OpHashMismatch; -- } -+ // if (msg.sender != ATLAS) revert AtlasErrors.InvalidCaller(); -+ // // Verify that the calldata injection came from the dApp frontend -+ // // and that the signatures are valid. -+ -+ // bytes32 _userOpHash = _getUserOperationHash(userOp, userOp.callConfig.allowsTrustedOpHash()); -+ -+ // { -+ // // Check user signature -+ // ValidCallsResult verifyUserResult = _verifyUser(dConfig, userOp, _userOpHash, msgSender, isSimulation); -+ // if (verifyUserResult != ValidCallsResult.Valid) { -+ // return verifyUserResult; -+ // } -+ -+ // // allowUnapprovedDAppSignatories still verifies signature match, but does not check -+ // // if dApp owner approved the signer. -+ // (ValidCallsResult verifyAuctioneerResult, bool allowUnapprovedDAppSignatories) = -+ // _verifyAuctioneer(dConfig, userOp, solverOps, dAppOp, msgSender); -+ -+ // if (verifyAuctioneerResult != ValidCallsResult.Valid && !isSimulation) { -+ // return verifyAuctioneerResult; -+ // } -+ + // // Check dapp signature + // ValidCallsResult verifyDappResult = + // _verifyDApp(dConfig, dAppOp, msgSender, allowUnapprovedDAppSignatories, isSimulation); @@ -209,78 +117,139 @@ diff -ruN ../src/contracts/atlas/AtlasVerification.sol contracts/atlas/AtlasVeri + // return verifyDappResult; + // } + // } -+ + +- // Check if the call configuration is valid +- ValidCallsResult _verifyCallConfigResult = _verifyCallConfig(dConfig.callConfig); +- if (_verifyCallConfigResult != ValidCallsResult.Valid) { +- return _verifyCallConfigResult; +- } + // // Check if the call configuration is valid + // ValidCallsResult _verifyCallConfigResult = _verifyCallConfig(dConfig.callConfig); + // if (_verifyCallConfigResult != ValidCallsResult.Valid) { + // return _verifyCallConfigResult; + // } -+ + +- // CASE: Solvers trust app to update content of UserOp after submission of solverOp +- if (dConfig.callConfig.allowsTrustedOpHash()) { +- // SessionKey must match explicitly - cannot be skipped +- if (userOp.sessionKey != dAppOp.from && !isSimulation) { +- return ValidCallsResult.InvalidAuctioneer; +- } + // // CASE: Solvers trust app to update content of UserOp after submission of solverOp + // if (dConfig.callConfig.allowsTrustedOpHash()) { + // // SessionKey must match explicitly - cannot be skipped + // if (userOp.sessionKey != dAppOp.from && !isSimulation) { + // return ValidCallsResult.InvalidAuctioneer; + // } -+ + +- // msgSender (the bundler) must be userOp.from, userOp.sessionKey / dappOp.from, or dappOp.bundler +- if (!(msgSender == dAppOp.from || msgSender == dAppOp.bundler || msgSender == userOp.from) && !isSimulation) +- { +- return ValidCallsResult.InvalidBundler; +- } +- } + // // msgSender (the bundler) must be userOp.from, userOp.sessionKey / dappOp.from, or dappOp.bundler + // if (!(msgSender == dAppOp.from || msgSender == dAppOp.bundler || msgSender == userOp.from) && !isSimulation) + // { + // return ValidCallsResult.InvalidBundler; + // } + // } -+ + +- uint256 _solverOpCount = solverOps.length; + // uint256 _solverOpCount = solverOps.length; -+ + +- { +- // Check number of solvers not greater than max, to prevent overflows in `solverIndex` +- if (_solverOpCount > _MAX_SOLVERS) { +- return ValidCallsResult.TooManySolverOps; +- } + // { + // // Check number of solvers not greater than max, to prevent overflows in `solverIndex` + // if (_solverOpCount > _MAX_SOLVERS) { + // return ValidCallsResult.TooManySolverOps; + // } -+ + +- // Check if past user's deadline +- if (userOp.deadline != 0 && block.number > userOp.deadline) { +- return ValidCallsResult.UserDeadlineReached; +- } + // // Check if past user's deadline + // if (userOp.deadline != 0 && block.number > userOp.deadline) { + // return ValidCallsResult.UserDeadlineReached; + // } -+ + +- // Check if past dapp's deadline +- if (dAppOp.deadline != 0 && block.number > dAppOp.deadline) { +- return ValidCallsResult.DAppDeadlineReached; +- } + // // Check if past dapp's deadline + // if (dAppOp.deadline != 0 && block.number > dAppOp.deadline) { + // return ValidCallsResult.DAppDeadlineReached; + // } -+ + +- // Check gas price is within user's limit +- if (tx.gasprice > userOp.maxFeePerGas) { +- return ValidCallsResult.GasPriceHigherThanMax; +- } + // // Check gas price is within user's limit + // if (tx.gasprice > userOp.maxFeePerGas) { + // return ValidCallsResult.GasPriceHigherThanMax; + // } -+ + +- // Check that the value of the tx is greater than or equal to the value specified +- if (msgValue < userOp.value) { +- return ValidCallsResult.TxValueLowerThanCallValue; +- } + // // Check that the value of the tx is greater than or equal to the value specified + // if (msgValue < userOp.value) { + // return ValidCallsResult.TxValueLowerThanCallValue; + // } -+ + +- // Check the call config read at the start of the metacall is same as user expected (as set in userOp) +- if (dConfig.callConfig != userOp.callConfig) { +- return ValidCallsResult.CallConfigMismatch; +- } +- } + // // Check the call config read at the start of the metacall is same as user expected (as set in userOp) + // if (dConfig.callConfig != userOp.callConfig) { + // return ValidCallsResult.CallConfigMismatch; + // } + // } -+ + +- // Some checks are only needed when call is not a simulation +- if (isSimulation) { +- // Add all solver ops if simulation +- return ValidCallsResult.Valid; +- } + // // Some checks are only needed when call is not a simulation + // if (isSimulation) { + // // Add all solver ops if simulation + // return ValidCallsResult.Valid; + // } -+ + +- // Verify a solver was successfully verified. +- if (_solverOpCount == 0) { +- if (!dConfig.callConfig.allowsZeroSolvers()) { +- return ValidCallsResult.NoSolverOp; +- } + // // Verify a solver was successfully verified. + // if (_solverOpCount == 0) { + // if (!dConfig.callConfig.allowsZeroSolvers()) { + // return ValidCallsResult.NoSolverOp; + // } -+ + +- if (dConfig.callConfig.needsFulfillment()) { +- return ValidCallsResult.NoSolverOp; +- } +- } + // if (dConfig.callConfig.needsFulfillment()) { + // return ValidCallsResult.NoSolverOp; + // } + // } -+ + +- if (_userOpHash != dAppOp.userOpHash) { +- return ValidCallsResult.OpHashMismatch; +- } + // if (_userOpHash != dAppOp.userOpHash) { + // return ValidCallsResult.OpHashMismatch; + // } @@ -288,8 +257,8 @@ diff -ruN ../src/contracts/atlas/AtlasVerification.sol contracts/atlas/AtlasVeri return ValidCallsResult.Valid; } diff -ruN ../src/contracts/atlas/Escrow.sol contracts/atlas/Escrow.sol ---- ../src/contracts/atlas/Escrow.sol 2024-11-26 17:59:53.000000000 +0530 -+++ contracts/atlas/Escrow.sol 2024-12-11 17:41:10.000000000 +0530 +--- ../src/contracts/atlas/Escrow.sol 2024-12-21 01:46:37 ++++ contracts/atlas/Escrow.sol 2024-12-21 14:13:19 @@ -451,7 +451,12 @@ // Get the uint256 from the memory array assembly { @@ -304,7 +273,43 @@ diff -ruN ../src/contracts/atlas/Escrow.sol contracts/atlas/Escrow.sol } return bidAmount; } -@@ -625,24 +630,34 @@ +@@ -533,12 +538,20 @@ + (bool _success, bytes memory _data) = + address(this).call{ gas: gasLimit }(abi.encodeCall(this.solverCall, (ctx, solverOp, bidAmount, returnData))); + +- if (_success) { ++ // SG: Start munging (case split) ++ require(_success); ++ ++ // if (_success) { + // If solverCall() was successful, intentionally leave uint256 result unset as 0 indicates success. + solverTracker = abi.decode(_data, (SolverTracker)); +- } else { +- // If solverCall() failed, catch the error and encode the failure case in the result uint accordingly. +- bytes4 _errorSwitch = bytes4(_data); ++ // } else { ++ // // If solverCall() failed, catch the error and encode the failure case in the result uint accordingly. ++ // bytes4 _errorSwitch = bytes4(_data); ++ // result = errorSwitch(_errorSwitch); ++ // } ++ } ++ ++ function errorSwitch(bytes4 _errorSwitch) internal returns (uint256 result){ + if (_errorSwitch == AlteredControl.selector) { + result = 1 << uint256(SolverOutcome.AlteredControl); + } else if (_errorSwitch == InsufficientEscrow.selector) { +@@ -563,9 +576,8 @@ + } else { + result = 1 << uint256(SolverOutcome.EVMError); + } +- } + } +- ++ + /// @notice Executes the SolverOperation logic, including preSolver and postSolver hooks via the Execution + /// Environment, as well as the actual solver call directly from Atlas to the solver contract. + /// @param ctx The Context struct containing lock data and the Execution Environment address. +@@ -625,24 +637,34 @@ if (!_borrow(solverOp.value)) revert InsufficientEscrow(); // Optimism's SafeCall lib allows us to limit how much returndata gets copied to memory, to prevent OOG attacks. @@ -353,8 +358,8 @@ diff -ruN ../src/contracts/atlas/Escrow.sol contracts/atlas/Escrow.sol // ------------------------------------- // // Post-Solver Call // diff -ruN ../src/contracts/atlas/FactoryLib.sol contracts/atlas/FactoryLib.sol ---- ../src/contracts/atlas/FactoryLib.sol 2024-11-26 17:59:53.000000000 +0530 -+++ contracts/atlas/FactoryLib.sol 2024-12-02 15:58:20.000000000 +0530 +--- ../src/contracts/atlas/FactoryLib.sol 2024-12-21 01:46:37 ++++ contracts/atlas/FactoryLib.sol 2024-12-21 01:46:37 @@ -49,7 +49,9 @@ ) ) @@ -366,9 +371,48 @@ diff -ruN ../src/contracts/atlas/FactoryLib.sol contracts/atlas/FactoryLib.sol if (executionEnvironment.code.length == 0) { assembly { executionEnvironment := create2(0, add(_creationCode, 32), mload(_creationCode), salt) +diff -ruN ../src/contracts/atlas/Storage.sol contracts/atlas/Storage.sol +--- ../src/contracts/atlas/Storage.sol 2024-12-21 14:33:52 ++++ contracts/atlas/Storage.sol 2024-12-21 01:46:37 +@@ -31,7 +31,7 @@ + uint256 public constant SCALE = AccountingMath._SCALE; + uint256 public constant FIXED_GAS_OFFSET = AccountingMath._FIXED_GAS_OFFSET; + +- // Transient storage slots ++ // transient storage slots + uint256 internal transient t_lock; // contains activeAddress, callConfig, and phase + uint256 internal transient t_solverLock; + address internal transient t_solverTo; // current solverOp.solver contract address +@@ -131,7 +131,7 @@ + } + + // ---------------------------------------------------- // +- // Transient External Getters // ++ // transient External Getters // + // ---------------------------------------------------- // + + function lock() external view returns (address activeEnvironment, uint32 callConfig, uint8 phase) { +@@ -153,7 +153,7 @@ + } + + // ---------------------------------------------------- // +- // Transient Internal Getters // ++ // transient Internal Getters // + // ---------------------------------------------------- // + + function _lock() internal view returns (address activeEnvironment, uint32 callConfig, uint8 phase) { +@@ -194,7 +194,7 @@ + } + + // ---------------------------------------------------- // +- // Transient Setters // ++ // transient Setters // + // ---------------------------------------------------- // + + function _setLock(address activeEnvironment, uint32 callConfig, uint8 phase) internal { diff -ruN ../src/contracts/solver/SolverBase.sol contracts/solver/SolverBase.sol ---- ../src/contracts/solver/SolverBase.sol 2024-12-11 20:21:48.000000000 +0530 -+++ contracts/solver/SolverBase.sol 2024-12-11 20:33:09.000000000 +0530 +--- ../src/contracts/solver/SolverBase.sol 2024-12-21 01:46:37 ++++ contracts/solver/SolverBase.sol 2024-12-21 01:46:37 @@ -50,8 +50,11 @@ safetyFirst(executionEnvironment, solverOpFrom) payBids(executionEnvironment, bidToken, bidAmount) diff --git a/certora/confs/Atlas_transient.conf b/certora/confs/Atlas_transient.conf index dcf7f3f5..57bcc99e 100644 --- a/certora/confs/Atlas_transient.conf +++ b/certora/confs/Atlas_transient.conf @@ -1,59 +1,56 @@ { - "assert_autofinder_success": true, - "commit_sha1": "6755ba8d172e3e4ca2cb0be03110771032861103", - "files": [ - "certora/harnesses/AtlasHarness.sol", - "certora/munged/contracts/examples/fastlane-online/FastLaneControl.sol:FastLaneOnlineControl", - //"certora/munged/contracts/solver/src/TestSolver.sol:Solver", - "certora/munged/contracts/atlas/AtlasVerification.sol", - "certora/munged/contracts/atlas/FactoryLib.sol", - //"certora/munged/contracts/dapp/DAppControl.sol", - "certora/munged/contracts/examples/fastlane-online/FastLaneControl.sol:FastLaneOnlineControl", - "lib/solady/src/utils/SafeTransferLib.sol", - "certora/munged/contracts/common/ExecutionEnvironment.sol", - "certora/munged/contracts/solver/SolverBase.sol", - //"certora/harnesses/ERC20Like/DummyWeth.sol", - //"certora/harnesses/Utilities.sol", - - - "certora/munged/contracts/gasCalculator/BaseGasCalculator.sol", - ], - "link": [ - "AtlasHarness:VERIFICATION=AtlasVerification", - "AtlasHarness:FACTORY_LIB=FactoryLib", - "AtlasHarness:L2_GAS_CALCULATOR=BaseGasCalculator", - //"Solver:_atlas=AtlasHarness" - - ], - "parametric_contracts": [ + "assert_autofinder_success": true, + "build_cache": true, + "files": [ + "certora/harnesses/AtlasHarness.sol", + "certora/munged/contracts/examples/fastlane-online/FastLaneControl.sol:FastLaneOnlineControl", + "certora/munged/contracts/atlas/AtlasVerification.sol", + "certora/munged/contracts/atlas/FactoryLib.sol", + "certora/munged/contracts/examples/fastlane-online/FastLaneControl.sol:FastLaneOnlineControl", + "lib/solady/src/utils/SafeTransferLib.sol", + "certora/munged/contracts/common/ExecutionEnvironment.sol", + "certora/munged/contracts/solver/SolverBase.sol", + "certora/munged/contracts/gasCalculator/BaseGasCalculator.sol" + ], + "link": [ + "AtlasHarness:VERIFICATION=AtlasVerification", + "AtlasHarness:FACTORY_LIB=FactoryLib", + "AtlasHarness:L2_GAS_CALCULATOR=BaseGasCalculator" + ], + "loop_iter": "1", + "msg": "Atlas", + "optimistic_fallback": true, + "optimistic_loop": true, + "packages": [ + "ds-test/=lib/forge-std/lib/ds-test/src/", + "eth-gas-reporter/=node_modules/eth-gas-reporter/", + "forge-std/=lib/forge-std/src/", + "hardhat/=node_modules/hardhat/", + "openzeppelin-contracts-upgradeable/=lib/openzeppelin-contracts-upgradeable/", + "openzeppelin-contracts/=lib/openzeppelin-contracts/", + "@openzeppelin/=lib/openzeppelin-contracts/", + "solady/=lib/solady/src/" + ], + "parametric_contracts": [ "AtlasHarness" ], - "java_args": [ - " -ea -Dlevel.setup.helpers=info" - ], - "msg": "Atlas", - //"rule_sanity":"basic", - "packages": [ - "ds-test/=lib/forge-std/lib/ds-test/src/", - "eth-gas-reporter/=node_modules/eth-gas-reporter/", - "forge-std/=lib/forge-std/src/", - "hardhat/=node_modules/hardhat/", - "openzeppelin-contracts-upgradeable/=lib/openzeppelin-contracts-upgradeable/", - "openzeppelin-contracts/=lib/openzeppelin-contracts/", - "@openzeppelin/=lib/openzeppelin-contracts/", - "solady/=lib/solady/src/", - ], - "process": "emv", - "prover_args": [ - "-destructiveOptimizations twostage -s [z3:def] -callTraceHardFail on -maxCommandCount 1000000000 -maxBlockCount 1000000000 -globallyRelaxedPointerSemantics true -depth 6 -smt_initialSplitDepth 6" - ], - "loop_iter": "1", - "optimistic_loop": true, - "optimistic_fallback": true, - "smt_timeout":"7200", - "global_timeout":"7200", - "solc": "solc8.28", - "solc_optimize": "50", - "solc_via_ir": true, - "verify": "AtlasHarness:certora/specs/Atlas_transient.spec" + "process": "emv", + "prover_args": [ + "-destructiveOptimizations twostage", + "-s [z3:def]", + "-callTraceHardFail on", + "-maxCommandCount 1000000000", + "-maxBlockCount 1000000000", + "-globallyRelaxedPointerSemantics true", + "-depth 6", + "-smt_initialSplitDepth 1", + "-optimizeAfterSplits 1" + ], + "commit_sha1": "10f5d9ce5d42d95ffb13d14252133560219904a7", + "server": "prover", + "smt_timeout": "600", + "solc": "solc8.28", + "solc_optimize": "50", + "solc_via_ir": true, + "verify": "AtlasHarness:certora/specs/Atlas_transient.spec" } \ No newline at end of file diff --git a/certora/shelly.md b/certora/shelly.md new file mode 100644 index 00000000..07c920a9 --- /dev/null +++ b/certora/shelly.md @@ -0,0 +1,12 @@ +yarn +git submodule init +git submodule update +cd certora +make munged + +# need to define a process for fixing dependencies + +atlasEthBalanceGeSumAccountsSurchargeTransientMetacallRule +invariant atlasEthBalanceGeSumAccountsSurcharge* - 4 cases + metacall requires reentrancy + try to havoc / strong invariant \ No newline at end of file diff --git a/certora/specs/Atlas.spec b/certora/specs/Atlas.spec index 8c4fd194..a58f9afe 100644 --- a/certora/specs/Atlas.spec +++ b/certora/specs/Atlas.spec @@ -9,7 +9,7 @@ methods{ function _.initialGasUsed(uint256) external => NONDET; function _._computeSalt(address, address, uint32) internal => NONDET; function CallBits.exPostBids(uint32) internal returns bool => ALWAYS(false); - function AtlasVerification.verifySolverOp(Atlas.SolverOperation, bytes32 ,uint256, address, bool) external returns uint256 => NONDET; + function AtlasVerification.verifySolverOp(Atlas.SolverOperation, bytes32 ,uint256, address, bool) external returns uint256 => NONDET; // xxx function Escrow._checkSolverBidToken(address, address, uint256) internal returns uint256 => NONDET; function Escrow._validateSolverOpDeadline(Atlas.SolverOperation calldata, Atlas.DAppConfig memory) internal returns uint256 => NONDET; function Escrow._checkTrustedOpHash(Atlas.DAppConfig memory, bool, Atlas.UserOperation calldata, Atlas.SolverOperation calldata, uint256) internal returns uint256 => NONDET; @@ -21,7 +21,7 @@ methods{ function getLockEnv() external returns address envfree; function getLockCallConfig() external returns uint32 envfree; function getLockPhase() external returns uint8 envfree; - function Escrow._solverOpWrapper(Atlas.Context memory, Atlas.SolverOperation calldata, uint256, uint256, bytes memory) internal returns (uint256, Atlas.SolverTracker memory) => borrowReconcileCVL(); + function Escrow._solverOpWrapper(Atlas.Context memory, Atlas.SolverOperation calldata, uint256, uint256, bytes memory) internal returns (uint256, Atlas.SolverTracker memory) => borrowReconcileCVL(); // xxx // checking if this avoids the failed to locate function error // function _._allocateValueCall(address, uint256, bytes calldata) internal => NONDET; diff --git a/certora/specs/Atlas_transient.spec b/certora/specs/Atlas_transient.spec index a4ce12d0..dc42fc1e 100644 --- a/certora/specs/Atlas_transient.spec +++ b/certora/specs/Atlas_transient.spec @@ -6,7 +6,7 @@ methods{ function _.CALL_CONFIG() external => DISPATCHER(true); function _.getDAppConfig(Atlas.UserOperation) external => NONDET; - function _.initialGasUsed(uint256) external => NONDET; + // function _.initialGasUsed(uint256) external => NONDET; function _._computeSalt(address, address, uint32) internal => NONDET; //false would lead down the bidKnownIteration path which is simpler function CallBits.exPostBids(uint32) internal returns bool => ALWAYS(false); @@ -16,9 +16,21 @@ methods{ function Escrow._checkTrustedOpHash(Atlas.DAppConfig memory, bool, Atlas.UserOperation calldata, Atlas.SolverOperation calldata, uint256) internal returns uint256 => NONDET; function GasAccounting._updateAnalytics(Atlas.EscrowAccountAccessData memory, bool, uint256) internal => NONDET; function Factory._getOrCreateExecutionEnvironment(address, address, uint32) internal returns address => NONDET; - function _.getCalldataCost(uint256) external => CONSTANT; + function _.getCalldataCost(uint256 l) external => calldataCostGhost[l] expect (uint256) ALL; + function _._getCalldataCost(uint256 l) internal => calldataCostGhost[l] expect (uint256); // why ext summary wasn't applied? because we needed all. but the wrapper also isn't needed + function _.initialGasUsed(uint256 l) external => initialGasUsed[l] expect (uint256) ALL; function GasAccounting._settle(Atlas.Context memory, uint256, address) internal returns (uint256, uint256) => settleCVL(); function Escrow.errorSwitch(bytes4) internal returns (uint256) => NONDET; + function EscrowBits.canExecute(uint256) internal returns (bool) => ALWAYS(true); + // function Escrow._solverOpWrapper(Atlas.Context memory, Atlas.SolverOperation calldata, uint256, uint256, bytes memory) internal returns (uint256, Atlas.SolverTracker memory) => nothingSolverOp(); + + function _.preOpsWrapper(Atlas.UserOperation) external => NONDET; + function _.userWrapper(Atlas.UserOperation) external => NONDET; + function _.solverPreTryCatch(uint256,Atlas.SolverOperation,bytes) external => NONDET; + function _.atlasSolverCall(address,address,address,uint256,bytes,bytes) external => NONDET; + function _.solverPostTryCatch(Atlas.SolverOperation,bytes,Atlas.SolverTracker) external => NONDET; + function _.allocateValue(address,uint256,bytes) external => NONDET; // SG xxx may contribute balance to Atlas, use better summary + function _.postOpsWrapper(bool,bytes) external => NONDET; // getters function getLockEnv() external returns address envfree; @@ -54,10 +66,21 @@ methods{ // FastLaneOnlineControl.postOpsCall(bool, bytes) // ] default HAVOC_ALL; } + +function nothingSolverOp() returns (uint256, Atlas.SolverTracker){ + uint256 result; + Atlas.SolverTracker solverTracker; + + return (result, solverTracker); +} + + /*---------------------------------------------------------------------------------------------------------------- GHOSTS & HOOKS ----------------------------------------------------------------------------------------------------------------*/ +ghost mapping(uint256 => uint256) calldataCostGhost; +ghost mapping(uint256 => uint256) initialGasUsed; // ghost tracking the sum of atlETH bonded balances persistent ghost mathint sumOfBonded{ @@ -216,6 +239,8 @@ rule atlasEthBalanceGeSumAccountsSurchargeTransientMetacallRule(){ env e; require e.msg.sender != currentContract; + // invariant atlasEthBalanceEqSumAccountsSurchargeMetacall() + // nativeBalances[currentContract] == sumOfBonded + sumOfUnbonded + sumOfUnbonding + currentContract.S_cumulativeSurcharge require nativeBalances[currentContract] >= sumOfBonded + sumOfUnbonded + sumOfUnbonding + currentContract.S_cumulativeSurcharge + deposits - withdrawals; // Atlas.UserOperation userOp;