remove separating v1.5 folder, which was there just for project organ…

…ization, and adding all the specs to the spec folder and all the confs to the conf folder
Certora · Jan 7, 2025 · 91d4f0d · 91d4f0d
1 parent 7500134
commit 91d4f0d
Show file tree

Hide file tree

Showing 10 changed files with 5 additions and 34 deletions.
diff --git a/certora/conf/v1.5/execute.conf → certora/conf/execute.conf b/certora/conf/v1.5/execute.conf → 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 → certora/conf/fallback.conf b/certora/conf/v1.5/fallback.conf → 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 → certora/conf/guards.conf b/certora/conf/v1.5/guards.conf → 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 → certora/conf/hash.conf b/certora/conf/v1.5/hash.conf → 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 → certora/conf/setup.conf b/certora/conf/v1.5/setup.conf → 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 → certora/specs/Execute.spec b/certora/specs/v1.5/Execute.spec → 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 → certora/specs/Fallback.spec b/certora/specs/v1.5/Fallback.spec → 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,23 +41,20 @@ 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 { 
         f -> f.selector != sig:simulateAndRevert(address,bytes).selector 
     }
 
 /// @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);
     assert lastReverted;
 }
 
 /// @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 → certora/specs/Guards.spec b/certora/specs/v1.5/Guards.spec → 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,15 +120,13 @@ 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
     assert (e.msg.sender == safe);
 }
 
 /// @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 → certora/specs/Hash.spec b/certora/specs/v1.5/Hash.spec → 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 → certora/specs/Setup.spec b/certora/specs/v1.5/Setup.spec → 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,