Adding General Rules

CVLByExamples/GeneralExamples/certora/conf/generalRules_ERC20.conf

@@ -0,0 +1,9 @@
+{
+  "files": [
+    "contracts/ERC20.sol:ERC20",
+    "certora/helpersContracts/ERC20helper.sol:ERC20Helper"
+  ],
+  "verify": "ERC20:certora/spec/general.spec",
+  "solc": "solc8.17",
+  "msg": "genral Rules on ERC20 contract"
+}

CVLByExamples/GeneralExamples/certora/conf/generalRules_VAULT.conf

@@ -0,0 +1,10 @@
+{
+  "files": [
+    "contracts/Vault.sol:Vault",
+    "contracts/ERC20.sol:ERC20",
+    "certora/helpersContracts/ERC20helper.sol:ERC20Helper"
+  ],
+  "verify": "Vault:certora/spec/general.spec",
+  "solc": "solc8.17",
+  "msg": "genral Rules on Vault contract"
+}

CVLByExamples/GeneralExamples/certora/helpersContracts/ERC20Helper.sol

@@ -0,0 +1,10 @@
+// SPDX-License-Identifier: agpl-3.0
+pragma solidity ^0.8.0;
+import "../../contracts/IERC20.sol";
+
+contract ERC20Helper {
+
+    function tokenBalanceOf(address token, address user) public returns (uint256) {
+            return IERC20(token).balanceOf(user);
+    }
+}

CVLByExamples/GeneralExamples/certora/spec/general.spec

@@ -0,0 +1,122 @@
+using ERC20Helper as erc20helper;
+
+methods {
+    function _.name() external => DISPATCHER(true);
+    function _.symbol() external => DISPATCHER(true);
+    function _.decimals() external => DISPATCHER(true);
+    function _.totalSupply() external => DISPATCHER(true);
+    function _.balanceOf(address) external => DISPATCHER(true);
+    function _.allowance(address,address) external => DISPATCHER(true);
+    function _.approve(address,uint256) external => DISPATCHER(true);
+    function _.transfer(address,uint256) external => DISPATCHER(true);
+    function _.transferFrom(address,address,uint256) external => DISPATCHER(true);
+
+	function erc20helper.tokenBalanceOf(address, address) external returns (uint256) envfree;
+}
+
+/* 
+	Property: Find and show a path for each method.
+*/
+rule reachability(method f)
+{
+	env e;
+	calldataarg args;
+	f(e,args);
+	satisfy true;
+}
+
+/* 
+   	Property: Define and check functions that should never revert
+	Notice:  use f.selector to state which functions should not revert,e.g.f.selector == sig:balanceOf(address).selector 
+*/  
+definition nonReveritngFunction(method f ) returns bool = true; 
+
+rule noRevert(method f) filtered {f -> nonReveritngFunction(f) }
+{
+	env e;
+	calldataarg arg;
+    //consider auto filtering for non-payable functions 
+	require e.msg.value == 0; 
+	f@withrevert(e, arg); 
+	assert !lastReverted, "method should not revert";
+}
+
+
+/* 
+    Property: Checks if a function can be frontrun 
+    Notice: Can be enhanced to check more than one function as rules can be double-parameteric
+*/ 
+rule simpleFrontRunning(method f, method g) filtered { f-> !f.isView, g-> !g.isView }
+{
+	env e1;
+	calldataarg arg;
+
+	storage initialStorage = lastStorage;
+	f(e1, arg); 
+
+
+	env e2;
+	calldataarg arg2;
+	require e2.msg.sender != e1.msg.sender;
+	g(e2, arg2) at initialStorage; 
+
+	f@withrevert(e1, arg);
+	bool succeeded = !lastReverted;
+
+	assert succeeded, "should be called also if frontrunned";
+}
+
+
+/** 
+    @title -   This rule find which functions are privileged.
+    @notice A function is privileged if there is only one address that can call it.
+    @dev The rules finds this by finding which functions can be called by two different users.
+*/
+
+rule privilegedOperation(method f, address privileged)
+{
+	env e1;
+	calldataarg arg;
+	require e1.msg.sender == privileged;
+
+	storage initialStorage = lastStorage;
+	f@withrevert(e1, arg); // privileged succeeds executing candidate privileged operation.
+	bool firstSucceeded = !lastReverted;
+
+	env e2;
+	calldataarg arg2;
+	require e2.msg.sender != privileged;
+	f@withrevert(e2, arg2) at initialStorage; // unprivileged
+	bool secondSucceeded = !lastReverted;
+
+	assert  !(firstSucceeded && secondSucceeded), "function is privileged";
+}
+
+
+rule decreaseInSystemEth(method f) {
+
+    uint256 before = nativeBalances[currentContract];
+
+    env e;
+	calldataarg arg;
+    f(e, arg);
+
+    uint256 after = nativeBalances[currentContract];
+
+    assert after >= before ||  false ; /* fill in cases where eth can decrease */ 
+}
+
+
+rule decreaseInERC20(method f) {
+    address token;
+    uint256 before = erc20helper.tokenBalanceOf(token, currentContract);
+
+    env e;
+	calldataarg arg;
+    f(e, arg);
+
+    uint256 after = erc20helper.tokenBalanceOf(token, currentContract);
+
+    assert after >= before ||  false ; /* fill in cases eth can decrease */ 
+
+}