diff --git a/certora/conf/v1.5/execute.conf b/certora/conf/execute.conf similarity index 90% rename from certora/conf/v1.5/execute.conf rename to certora/conf/execute.conf index 3972e17c0..69af1c53d 100644 --- a/certora/conf/v1.5/execute.conf +++ b/certora/conf/execute.conf @@ -7,7 +7,7 @@ "link": [ ], - "verify": "SafeHarness:certora/specs/v1.5/Execute.spec", + "verify": "SafeHarness:certora/specs/Execute.spec", "assert_autofinder_success": true, "optimistic_summary_recursion": true, diff --git a/certora/conf/v1.5/fallback.conf b/certora/conf/fallback.conf similarity index 90% rename from certora/conf/v1.5/fallback.conf rename to certora/conf/fallback.conf index 4e7621973..1c8ecf8b3 100644 --- a/certora/conf/v1.5/fallback.conf +++ b/certora/conf/fallback.conf @@ -7,7 +7,7 @@ "link": [ ], - "verify": "SafeHarness:certora/specs/v1.5/Fallback.spec", + "verify": "SafeHarness:certora/specs/Fallback.spec", "assert_autofinder_success": true, "optimistic_summary_recursion": true, diff --git a/certora/conf/v1.5/guards.conf b/certora/conf/guards.conf similarity index 93% rename from certora/conf/v1.5/guards.conf rename to certora/conf/guards.conf index 6701a24a5..e367ba943 100644 --- a/certora/conf/v1.5/guards.conf +++ b/certora/conf/guards.conf @@ -10,7 +10,7 @@ "link": [ ], - "verify": "SafeHarness:certora/specs/v1.5/Guards.spec", + "verify": "SafeHarness:certora/specs/Guards.spec", "assert_autofinder_success": true, "optimistic_summary_recursion": true, diff --git a/certora/conf/v1.5/hash.conf b/certora/conf/hash.conf similarity index 89% rename from certora/conf/v1.5/hash.conf rename to certora/conf/hash.conf index 9e82324e9..527d89415 100644 --- a/certora/conf/v1.5/hash.conf +++ b/certora/conf/hash.conf @@ -5,7 +5,7 @@ "link": [ ], - "verify": "SafeHarness:certora/specs/v1.5/Hash.spec", + "verify": "SafeHarness:certora/specs/Hash.spec", "assert_autofinder_success": true, "optimistic_summary_recursion": true, diff --git a/certora/conf/v1.5/setup.conf b/certora/conf/setup.conf similarity index 89% rename from certora/conf/v1.5/setup.conf rename to certora/conf/setup.conf index 71a505028..8b0407ff0 100644 --- a/certora/conf/v1.5/setup.conf +++ b/certora/conf/setup.conf @@ -5,7 +5,7 @@ "link": [ ], - "verify": "SafeHarness:certora/specs/v1.5/Setup.spec", + "verify": "SafeHarness:certora/specs/Setup.spec", "assert_autofinder_success": true, "optimistic_summary_recursion": true, diff --git a/certora/specs/v1.5/Execute.spec b/certora/specs/Execute.spec similarity index 89% rename from certora/specs/v1.5/Execute.spec rename to certora/specs/Execute.spec index 38b2f91ac..778772dcb 100644 --- a/certora/specs/v1.5/Execute.spec +++ b/certora/specs/Execute.spec @@ -61,7 +61,6 @@ function execute_summary() returns bool { // ---- Rules ------------------------------------------------------------------ /// @dev a successful call to execTransactionFromModule must be from enabled module -/// @status Done: https://prover.certora.com/output/39601/dcc09acbeead4df9868519a4ac0e3ee5?anonymousKey=327efa3ac9dde7907db389b3a2688ce42094ef41 rule execTxnModulePermissions( address to, uint256 value, @@ -78,7 +77,6 @@ rule execTxnModulePermissions( } /// @dev a successful call to execTransactionFromModuleReturnData must be from enabled module -/// @status Done: https://prover.certora.com/output/39601/49c3745804084c5aa7284792f805316b?anonymousKey=356721ccd4d2592e83a5fbf1ee58ed278e8dd9ff rule execTxnModuleReturnDataPermissions( address to, uint256 value, @@ -96,7 +94,6 @@ rule execTxnModuleReturnDataPermissions( /// @dev execute can only be called by execTransaction or execTransactionFromModule -/// @status Done: https://prover.certora.com/output/39601/9b60b63b5aa84428b9fca530f870c4b6?anonymousKey=4b731a650337bea416faf81e806d96a7b040f8e8 rule executePermissions(method f) filtered { f -> f.selector != sig:simulateAndRevert(address,bytes).selector && f.selector != sig:getStorageAt(uint256,uint256).selector @@ -142,7 +139,6 @@ rule executePermissions(method f) filtered { /// @dev at least "threshold" signatures provided -/// @status Done: https://prover.certora.com/output/39601/9f364fac5e8c43e0acc2d93cea3f5560?anonymousKey=d37fb383bff8fa2fe0dacf60b61130e1aadf2ad4 rule executeThresholdMet( address to, uint256 value, diff --git a/certora/specs/v1.5/Fallback.spec b/certora/specs/Fallback.spec similarity index 78% rename from certora/specs/v1.5/Fallback.spec rename to certora/specs/Fallback.spec index 5f70e4afc..64c695b5c 100644 --- a/certora/specs/v1.5/Fallback.spec +++ b/certora/specs/Fallback.spec @@ -31,7 +31,6 @@ methods { // ---- Rules ------------------------------------------------------------------ /// @dev fallback handler gets set by setFallbackHandler -/// @status Done: https://prover.certora.com/output/39601/ab995049df0b454b888f3cd6a27331d5?anonymousKey=1a710fa917c8c60a9a420e026d6570d91e1e923b rule setFallbackIntegrity(address handler) { env e; @@ -42,7 +41,6 @@ rule setFallbackIntegrity(address handler) { } /// @dev invariant: the address in fallback handler slot is never self -/// @status Done: https://prover.certora.com/output/39601/edb75f86f23445cdbc7cd7b5c4c420b6?anonymousKey=62191f4f70404bcbce784f5172e3ed7ab323d416 invariant fallbackHandlerNeverSelf() getFallbackHandler() != safe filtered { @@ -50,7 +48,6 @@ invariant fallbackHandlerNeverSelf() } /// @dev for soundness of fallbackHandlerNeverSelf, we prove a rule that simulateAndRevert always reverts -/// @status Done: https://prover.certora.com/output/39601/38653935d0db460994d1a8c5bfdf57bb?anonymousKey=988218ca4f784fd27ea96fd2f14644719e2e9468 rule simulateAndRevertReverts(address caddr, bytes b) { env e; simulateAndRevert@withrevert(e,caddr,b); @@ -58,7 +55,6 @@ rule simulateAndRevertReverts(address caddr, bytes b) { } /// @dev setSafeMethod sets the handler -/// @status Done: https://prover.certora.com/output/39601/bab9860cdfc44a83bed82e79d8c06218?anonymousKey=b4c5dbef050bb201ad78b3dd5af5cdca8ffa9f92 rule setSafeMethodSets(bytes4 selector, address newMethodCaddr) { env e; @@ -72,8 +68,6 @@ rule setSafeMethodSets(bytes4 selector, address newMethodCaddr) { } /// @dev setSafeMethod removes the handler -/// @status Done: https://prover.certora.com/output/39601/8591535c4a434f3e826af00b95ea1ca8?anonymousKey=a7b6743a3161a3289883f99014619a9d6e7196e1 -/// note this is a special case of the rule above, but we still include it here for illustration rule setSafeMethodRemoves(bytes4 selector) { env e; @@ -87,7 +81,6 @@ rule setSafeMethodRemoves(bytes4 selector) { } /// @dev setSafeMethod changes the handler -/// @status Done: https://prover.certora.com/output/39601/b44efe9ef3bd4ff5a1af710a7d3d7ee4?anonymousKey=7fd15cc355164c803123c27b41660fed34548647 rule setSafeMethodChanges(bytes4 selector, address newMethodCaddr) { env e; @@ -105,7 +98,6 @@ rule setSafeMethodChanges(bytes4 selector, address newMethodCaddr) { /// @dev a handler, once set via setSafeMethod, is possible to call -/// @status Done: https://prover.certora.com/output/39601/9fcde04ecd434963b9ce788f7ddea8c1?anonymousKey=a7efde58b28ef7c99264424b66984a8d39b78518 rule handlerCallableIfSet(method f, bytes4 selector) filtered { f -> f.isFallback } { env e; @@ -128,7 +120,6 @@ rule handlerCallableIfSet(method f, bytes4 selector) filtered { f -> f.isFallbac } /// @dev a handler is called under expected conditions -/// @status Done: https://prover.certora.com/output/39601/a5bab5a7af8b4fd2819dedbc6e3221b9?anonymousKey=e4505515d8d69b3b1697c97fc3cc8f994802e46d rule handlerCalledIfSet() { env e; diff --git a/certora/specs/v1.5/Guards.spec b/certora/specs/Guards.spec similarity index 83% rename from certora/specs/v1.5/Guards.spec rename to certora/specs/Guards.spec index a39247fd6..b32999d70 100644 --- a/certora/specs/v1.5/Guards.spec +++ b/certora/specs/Guards.spec @@ -72,7 +72,6 @@ methods { // ---- Rules ------------------------------------------------------------------ /// @dev the only method that can change the guard is setGuard -/// @status Done: https://prover.certora.com/output/39601/a05e24787c68404d877ae4acce693734?anonymousKey=02030d2ca97a19d0d7a70deb5a91dc4b75bca89d rule guardAddressChange(method f) filtered { f -> f.selector != sig:simulateAndRevert(address,bytes).selector && f.selector != sig:getStorageAt(uint256,uint256).selector @@ -89,8 +88,6 @@ rule guardAddressChange(method f) filtered { } /// @dev the only method that can change the module guard is setModuleGuard -/// @status Done: https://prover.certora.com/output/39601/a05e24787c68404d877ae4acce693734?anonymousKey=02030d2ca97a19d0d7a70deb5a91dc4b75bca89d - rule moduleGuardAddressChange(method f) filtered { f -> f.selector != sig:simulateAndRevert(address,bytes).selector && f.selector != sig:getStorageAt(uint256,uint256).selector @@ -107,7 +104,6 @@ rule moduleGuardAddressChange(method f) filtered { } /// @dev set-get correspondence for (regular) guard -/// @status Done: https://prover.certora.com/output/39601/a05e24787c68404d877ae4acce693734?anonymousKey=02030d2ca97a19d0d7a70deb5a91dc4b75bca89d rule setGetCorrespondenceGuard(address guard) { env e; setGuard(e,guard); @@ -116,7 +112,6 @@ rule setGetCorrespondenceGuard(address guard) { } /// @dev set-get correspodnence for module guard -/// @status Done: https://prover.certora.com/output/39601/a05e24787c68404d877ae4acce693734?anonymousKey=02030d2ca97a19d0d7a70deb5a91dc4b75bca89d rule setGetCorrespondenceModuleGuard(address guard) { env e; setModuleGuard(e,guard); @@ -125,7 +120,6 @@ rule setGetCorrespondenceModuleGuard(address guard) { } /// @dev setGuard can only be called by contract itself. -/// @status Done: https://prover.certora.com/output/39601/b78bb57e77e444ad9d89861a8dc66e9f?anonymousKey=b6452b2c9f788d4a4dcd8d3c41f16a3e66e64a66 rule setGuardReentrant(address guard) { env e; setGuard(e,guard); // a successful call to setGuard @@ -133,7 +127,6 @@ rule setGuardReentrant(address guard) { } /// @dev setModuleGuard can only be called by contract itself. -/// @status Done: https://prover.certora.com/output/39601/8147e74eda404e61bcb6fc8e8849c5f3?anonymousKey=5c1e77468b6f5bff22c376894dca846f5ea83aab rule setModuleGuardReentrant(address guard) { env e; setModuleGuard(e,guard); @@ -142,7 +135,6 @@ rule setModuleGuardReentrant(address guard) { /// @dev the transaction guard gets called both pre- and post- any execTransaction -/// @status Done: https://prover.certora.com/output/39601/a9a8eaeba7994e10bf29dbe8813798b9?anonymousKey=fbddda2f78b44a7df3dff4707715b90b2d08ab63 rule txnGuardCalled( address to, uint256 value, @@ -176,7 +168,6 @@ rule txnGuardCalled( } /// @dev the module guard gets called both pre- and post- any execTransactionFromModule -/// @status Done: https://prover.certora.com/output/39601/7591e8c61e6d407b847e38bbe8238e13?anonymousKey=5d99429f5046e77825a4ed015af0a6a0d088538d rule moduleGuardCalled( address to, uint256 value, @@ -202,7 +193,6 @@ rule moduleGuardCalled( } /// @dev the module guard gets called both pre- and post- any execTransactionFromModuleReturnData -/// @status Done: https://prover.certora.com/output/39601/2de5a471d628464e8aaf4b9022e515de?anonymousKey=c4997fd77ba3808cf9bdc6a432f9b20eea551c95 rule moduleGuardCalledReturn( address to, uint256 value, diff --git a/certora/specs/v1.5/Hash.spec b/certora/specs/Hash.spec similarity index 81% rename from certora/specs/v1.5/Hash.spec rename to certora/specs/Hash.spec index 0e9b986dc..218ebdc4a 100644 --- a/certora/specs/v1.5/Hash.spec +++ b/certora/specs/Hash.spec @@ -17,8 +17,6 @@ methods { // ---- Rules ------------------------------------------------------------------ /// @dev approvedHashes[user][hash] can only be changed by msg.sender==user -/// @status Done: https://prover.certora.com/output/39601/bb515eafa67e4edd99bb5aa51a63877b?anonymousKey=9c42e3105c1c3a3fbc95c8a24fa43b3dd43a05d6 - rule approvedHashesUpdate(method f,bytes32 userHash,address user) filtered { f -> f.selector != sig:simulateAndRevert(address,bytes).selector } { @@ -38,8 +36,6 @@ rule approvedHashesUpdate(method f,bytes32 userHash,address user) filtered { /// @dev approvedHashes is set when calling approveHash -/// @status Done: https://prover.certora.com/output/39601/bb515eafa67e4edd99bb5aa51a63877b?anonymousKey=9c42e3105c1c3a3fbc95c8a24fa43b3dd43a05d6 - rule approvedHashesSet(bytes32 hashToApprove) { env e; approveHash(e,hashToApprove); diff --git a/certora/specs/v1.5/Setup.spec b/certora/specs/Setup.spec similarity index 89% rename from certora/specs/v1.5/Setup.spec rename to certora/specs/Setup.spec index 67217d450..9b413fd61 100644 --- a/certora/specs/v1.5/Setup.spec +++ b/certora/specs/Setup.spec @@ -17,8 +17,6 @@ methods { // ---- Rules ------------------------------------------------------------------ /// @dev setup can only be called if threshold = 0 and setup sets threshold > 0 -/// @status Done: https://prover.certora.com/output/39601/7849e9a464e042ea89bfe68fc226edbc?anonymousKey=5c1387afecb8bc86f23df3be5eb886a5cd82787f - rule setupThresholdZeroAndSetsPositiveThreshold( address[] _owners, uint256 _threshold,