Adding General Rules

CVLByExample/ConstantProductPool/certora/conf/runReentrancy.conf

@@ -0,0 +1,18 @@
+
+{
+  // files that are part of the scene (everything the Certora Prover can reason about)
+  "files": [
+    "contracts/correct/ConstantProductPoolFixed.sol:ConstantProductPool",
+    "contracts/DummyERC20A.sol",
+    "contracts/DummyERC20B.sol"
+  ],
+  // the main contract under test and the spec file 
+  "verify": "ConstantProductPool:../Reentrancy/certora/spec/noGuardSafety.spec",
+  // After unrolling loops, assume the loop halt conditions hold : https://docs.certora.com/en/latest/docs/prover/cli/options.html#options-regarding-source-code-loops 
+  "optimistic_loop": true,
+  // Makes the request to the prover but does not wait for verifications results
+  "send_only": true,
+  // msg to recognize this run (presented in your list of jobs under prover.cerotra.com)
+  "msg": "CVLExmaple: ConstantProductPool fixed version"
+}
+// alternatively, run `certoraRun contracts/broken/ConstantProductPoolBroken.sol:ConstantProductPool contracts/DummyERC20A.sol contracts/DummyERC20B.sol --verify ConstantProductPool:certora/spec/ConstantProductPool.spec --optimistic_loop --send_only --msg "CVLExmaple: ConstantProductPool fixed version"`

GenericRules/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"
+}

GenericRules/certora/conf/generalRules_Pool.conf

@@ -0,0 +1,13 @@
+{
+  "files": [
+    "contracts/Pool.sol",
+    "contracts/Asset.sol",
+  ],
+  "verify": "Pool:../spec/generalPool.spec",
+  "msg": "Pool with linking",
+  "link": [
+        "Pool:asset=Asset"
+    ],
+  "parametric_contracts": ["Pool"],
+  "rule_sanity": "basic"
+}

GenericRules/certora/conf/generalRules_VAULT.conf

@@ -0,0 +1,11 @@
+{
+  "files": [
+    "contracts/Vault.sol:Vault",
+ /// no need   "contracts/ERC20.sol:ERC20",
+    "certora/helpersContracts/ERC20helper.sol:ERC20Helper"
+  ],
+  "verify": "Vault:certora/spec/generalERC20.spec",
+  "solc": "solc8.17",
+  "prover_version": "jtoman/deleting-summaries",
+  "msg": "genral Rules on Vault contract with erc20 summ"
+}

GenericRules/certora/conf/test.conf

@@ -0,0 +1,9 @@
+{
+    "files": [
+        "contracts/ERC4626.sol",
+        "certora/helpersContracts/ERC20Helper.sol"
+    ],
+    "process": "emv",
+    "prover_version": "naftali/fix_calledContract_and_solidy_calls_in_summary",
+    "verify": "ERC4626:certora/spec/generalERC20.spec"
+}

GenericRules/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);
+    }
+}

GenericRules/certora/spec/erc20Summarization.spec

@@ -0,0 +1,68 @@
+methods {
+ //   function _.name() external => NONDET DELETE(true);
+ //   function _.symbol() external => NONDET DELETE(true);
+    function _.decimals() external => NONDET;
+    function _.totalSupply() external => erc20_totalSupply[calledContract] expect uint256 ;
+    function _.balanceOf(address u) external => erc20_balances[calledContract][u] expect uint256;
+    function _.allowance(address,address) external => NONDET; //TODO 
+    function _.approve(address,uint256) external => NONDET; //TODO
+    function _.transfer(address to, uint256 amount) external with (env e) => 
+                    erc20_transfer(calledContract, e, to, amount) expect bool;
+    function _.transferFrom(address from, address to, uint256 amount) external with (env e) => 
+                    erc20_transferFrom(calledContract, e, from, to, amount) expect bool;
+}
+/*
+methods {
+    function transfer(address to, uint256 amount) external returns (bool);
+}
+*/
+function erc20_transfer(address token, env e, address to, uint256 amount) returns bool {
+   /* if token == currentContract {
+        return transfer(e, to, amount);
+    }
+    else*/
+    if (erc20_balances[token][e.msg.sender] <  amount)
+        return false;
+    else {
+        erc20_balances[token][e.msg.sender] = assert_uint256(erc20_balances[token][e.msg.sender] - amount);
+        erc20_balances[token][to] = require_uint256(erc20_balances[token][to] + amount);
+        return true;
+    }
+
+}
+
+function erc20_transferFrom(address token, env e, address from, address to, uint256 amount) returns bool {
+   /* if token == currentContract {
+        return transferFrom(e, from, to, amount);
+    }
+    //todo allowance... 
+    else*/
+    if (erc20_balances[token][from] <  amount)
+        return false;
+    else {
+        erc20_balances[token][from] = assert_uint256(erc20_balances[token][from] - amount);
+        erc20_balances[token][to] = require_uint256(erc20_balances[token][to] + amount);
+        return true;
+    }
+
+}
+
+// tracking totalSupply for each erc20 address
+ghost mapping(address => uint256) erc20_totalSupply;
+
+// tracking balance for each erc20 address, a mapping for users to 
+ghost mapping(address => mapping(address => uint256)) erc20_balances;
+
+// tracking sum balance for each erc20 address, a mapping for users to 
+ghost mapping(address => uint256) erc20_sum_balances;
+
+
+// @title invariants to use as needed
+invariant sumBalancesIsTotalSupply() 
+     forall address t. erc20_sum_balances[t]==erc20_totalSupply[t];
+
+
+invariant sumBalancesIsTotalSupply() 
+    forall address t. forall address u. erc20_balances[t][u]<=erc20_totalSupply[t];
+
+

GenericRules/certora/spec/erc20Summarization2.spec

@@ -0,0 +1,68 @@
+methods {
+   // function _.name() external => NONDET DELETE(true);
+   // function _.symbol() external => NONDET DELETE(true);
+    function _.decimals() external => NONDET;
+    function _.totalSupply() external => erc20_totalSupply[calledContract] expect uint256 ;
+    function _.balanceOf(address u) external => erc20_balances[calledContract][u] expect uint256;
+    function _.allowance(address,address) external => NONDET; //TODO 
+    function _.approve(address,uint256) external => NONDET; //TODO
+    function _.transfer(address to, uint256 amount) external with (env e) => 
+                    erc20_transfer(calledContract, e, to, amount) expect bool;
+    function _.transferFrom(address from, address to, uint256 amount) external with (env e) => 
+                    erc20_transferFrom(calledContract, e, from, to, amount) expect bool;
+}
+
+methods {
+    function transfer(address to, uint256 amount) external returns (bool);
+}
+
+function erc20_transfer(address token, env e, address to, uint256 amount) returns bool {
+   if token == currentContract {
+        return transfer(e, to, amount);
+    }
+    else
+    if (erc20_balances[token][e.msg.sender] <  amount)
+        return false;
+    else {
+        erc20_balances[token][e.msg.sender] = assert_uint256(erc20_balances[token][e.msg.sender] - amount);
+        erc20_balances[token][to] = require_uint256(erc20_balances[token][to] + amount);
+        return true;
+    }
+
+}
+
+function erc20_transferFrom(address token, env e, address from, address to, uint256 amount) returns bool {
+   if token == currentContract {
+        return transferFrom(e, from, to, amount);
+    }
+    //todo allowance... 
+    else 
+    if (erc20_balances[token][from] <  amount)
+        return false;
+    else {
+        erc20_balances[token][from] = assert_uint256(erc20_balances[token][from] - amount);
+        erc20_balances[token][to] = require_uint256(erc20_balances[token][to] + amount);
+        return true;
+    }
+
+}
+
+// tracking totalSupply for each erc20 address
+ghost mapping(address => uint256) erc20_totalSupply;
+
+// tracking balance for each erc20 address, a mapping for users to 
+ghost mapping(address => mapping(address => uint256)) erc20_balances;
+
+// tracking sum balance for each erc20 address, a mapping for users to 
+ghost mapping(address => uint256) erc20_sum_balances;
+
+
+// @title invariants to use as needed
+invariant sumBalancesIsTotalSupply() 
+     forall address t. erc20_sum_balances[t]==erc20_totalSupply[t];
+
+
+invariant singleBalance() 
+    forall address t. forall address u. erc20_balances[t][u]<=erc20_totalSupply[t];
+
+

GenericRules/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 */ 
+
+}