Move certora helpers to a dedicated folder (#4211)

certora/specs/AccessControl.spec

@@ -1,4 +1,4 @@
-import "helpers.spec"
+import "helpers/helpers.spec"
 import "methods/IAccessControl.spec"
 
 /*

certora/specs/DoubleEndedQueue.spec

@@ -1,4 +1,4 @@
-import "helpers.spec"
+import "helpers/helpers.spec"
 
 methods {
     pushFront(bytes32)                    envfree
@@ -10,7 +10,7 @@ methods {
     // exposed for FV
     begin()             returns (int128)  envfree
     end()               returns (int128)  envfree
-    
+
     // view
     length()            returns (uint256) envfree
     empty()             returns (bool)    envfree
@@ -35,7 +35,7 @@ function max_int128() returns mathint {
 
 // Could be broken in theory, but not in practice
 function boundedQueue() returns bool {
-    return 
+    return
         max_int128() > to_mathint(end()) &&
         min_int128() < to_mathint(begin());
 }
@@ -78,11 +78,11 @@ invariant emptiness()
 invariant queueEndings()
     at_(length() - 1) == back() && at_(0) == front()
     filtered { f -> !f.isView }
-    { 
-        preserved { 
-            requireInvariant boundariesConsistency(); 
-            require boundedQueue(); 
-        } 
+    {
+        preserved {
+            requireInvariant boundariesConsistency();
+            require boundedQueue();
+        }
     }
 
 /*
@@ -94,12 +94,12 @@ rule pushFront(bytes32 value) {
     require boundedQueue();
 
     uint256 lengthBefore = length();
-    
+
     pushFront@withrevert(value);
-    
+
     // liveness
     assert !lastReverted, "never reverts";
-    
+
     // effect
     assert front() == value, "front set to value";
     assert length() == lengthBefore + 1, "queue extended";
@@ -134,12 +134,12 @@ rule pushBack(bytes32 value) {
     require boundedQueue();
 
     uint256 lengthBefore = length();
-    
+
     pushBack@withrevert(value);
-    
+
     // liveness
     assert !lastReverted, "never reverts";
-    
+
     // effect
     assert back() == value, "back set to value";
     assert length() == lengthBefore + 1, "queue increased";
@@ -205,7 +205,7 @@ rule popFrontConsistency(uint256 index) {
 
     // try to read value
     bytes32 after = at_@withrevert(index - 1);
-    
+
     assert !lastReverted, "value still exists in the queue";
     assert before == after, "values are offset and not modified";
 }
@@ -250,7 +250,7 @@ rule popBackConsistency(uint256 index) {
 
     // try to read value
     bytes32 after = at_@withrevert(index);
-    
+
     assert !lastReverted, "value still exists in the queue";
     assert before == after, "values are offset and not modified";
 }
@@ -262,10 +262,10 @@ rule popBackConsistency(uint256 index) {
 */
 rule clear {
     clear@withrevert();
-    
+
     // liveness
     assert !lastReverted, "never reverts";
-    
+
     // effect
     assert length() == 0, "sets length to 0";
 }

certora/specs/ERC20.spec

@@ -1,4 +1,4 @@
-import "helpers.spec"
+import "helpers/helpers.spec"
 import "methods/IERC20.spec"
 import "methods/IERC2612.spec"
 

certora/specs/ERC20FlashMint.spec

@@ -1,4 +1,4 @@
-import "helpers.spec"
+import "helpers/helpers.spec"
 import "methods/IERC20.spec"
 import "methods/IERC3156.spec"
 

certora/specs/ERC20Wrapper.spec

@@ -1,4 +1,4 @@
-import "helpers.spec"
+import "helpers/helpers.spec"
 import "ERC20.spec"
 
 methods {

certora/specs/ERC721.spec

@@ -1,4 +1,4 @@
-import "helpers.spec"
+import "helpers/helpers.spec"
 import "methods/IERC721.spec"
 
 methods {

certora/specs/EnumerableMap.spec

@@ -1,4 +1,4 @@
-import "helpers.spec"
+import "helpers/helpers.spec"
 
 methods {
     // library

certora/specs/EnumerableSet.spec

@@ -1,4 +1,4 @@
-import "helpers.spec"
+import "helpers/helpers.spec"
 
 methods {
     // library

certora/specs/Initializable.spec

@@ -1,4 +1,4 @@
-import "helpers.spec"
+import "helpers/helpers.spec"
 
 methods {
     // initialize, reinitialize, disable

certora/specs/Ownable.spec

@@ -1,4 +1,4 @@
-import "helpers.spec"
+import "helpers/helpers.spec"
 import "methods/IOwnable.spec"
 
 methods {

certora/specs/Ownable2Step.spec

@@ -1,4 +1,4 @@
-import "helpers.spec"
+import "helpers/helpers.spec"
 import "methods/IOwnable2Step.spec"
 
 methods {

certora/specs/Pausable.spec

@@ -1,4 +1,4 @@
-import "helpers.spec"
+import "helpers/helpers.spec"
 
 methods {
     paused() returns (bool) envfree
@@ -22,7 +22,7 @@ rule pause(env e) {
     bool success = !lastReverted;
 
     bool pausedAfter = paused();
-    
+
     // liveness
     assert success <=> !pausedBefore, "works if and only if the contract was not paused before";
 
@@ -44,7 +44,7 @@ rule unpause(env e) {
     bool success = !lastReverted;
 
     bool pausedAfter = paused();
-    
+
     // liveness
     assert success <=> pausedBefore, "works if and only if the contract was paused before";
 
@@ -71,7 +71,7 @@ rule whenPaused(env e) {
 */
 rule whenNotPaused(env e) {
     require nonpayable(e);
-    
+
     onlyWhenNotPaused@withrevert(e);
     assert !lastReverted <=> !paused(), "works if and only if the contract is not paused";
 }

certora/specs/TimelockController.spec

@@ -1,4 +1,4 @@
-import "helpers.spec"
+import "helpers/helpers.spec"
 import "methods/IAccessControl.spec"
 
 methods {