Rule quality examples

RuleQuality/Manager/Manager.sol

@@ -0,0 +1,52 @@
+
+contract Manager {
+
+	struct ManagedFund {
+        // The current manager of the fund
+        address currentManager;
+        // Management can be transferred, however the new manager needs to claim the management after being set as pending manager.
+        address pendingManager;
+		// amount managed
+		uint256 amount;
+	}
+
+	// Maps a fundId to its struct
+	mapping (uint256 => ManagedFund) public funds; 
+
+	// A flag indicating if an address is a current manager
+	mapping (address => bool) public isActiveManager; 
+
+
+	function createFund(uint256 fundId) public {
+		require(msg.sender != address(0));
+		require(funds[fundId].currentManager == address(0));
+		require(!isActiveManager[msg.sender]);
+		funds[fundId].currentManager = msg.sender;
+		isActiveManager[msg.sender] = true;
+	}
+
+
+	function setPendingManager(uint256 fundId, address pending) public {
+		require(funds[fundId].currentManager == msg.sender);
+		funds[fundId].pendingManager = pending;
+	}
+
+
+	function claimManagement(uint256 fundId) public {
+		require(msg.sender != address(0) && funds[fundId].currentManager != address(0));
+		require(funds[fundId].pendingManager == msg.sender);
+		require(!isActiveManager[msg.sender]);
+		isActiveManager[funds[fundId].currentManager] = false;
+		funds[fundId].currentManager = msg.sender;
+		funds[fundId].pendingManager = address(0);
+		isActiveManager[msg.sender] = true;
+	}
+
+	function getCurrentManager(uint256 fundId) public view returns (address) {
+		return funds[fundId].currentManager;
+	}
+
+	function getPendingManager(uint256 fundId) public view returns (address) {
+		return funds[fundId].pendingManager;
+	}
+}

RuleQuality/Manager/Manager.spec

@@ -0,0 +1,94 @@
+methods {
+		function getCurrentManager(uint256 fundId) external returns (address) envfree;
+		function getPendingManager(uint256 fundId) external returns (address) envfree;
+		function isActiveManager(address a) external returns (bool) envfree;
+}
+
+invariant ManagerZeroIsNotActive()
+		!isActiveManager(0);
+
+invariant tautologyInv()
+        !isActiveManager(0) <=> isActiveManager(0)==false ;
+
+
+
+rule uniqueManager(uint256 fundId1, uint256 fundId2, method f) {
+	require fundId1 != fundId2;
+    requireInvariant ManagerZeroIsNotActive();
+    require getCurrentManager(fundId1) != 0 => isActiveManager(getCurrentManager(fundId1));
+	require getCurrentManager(fundId2) != 0 => isActiveManager(getCurrentManager(fundId2));
+	require getCurrentManager(fundId1) != getCurrentManager(fundId2) ;
+
+	env e;
+	if (f.selector == sig:claimManagement(uint256).selector)
+	{
+		uint256 id;
+		/// Advanced sanity check:
+		/// Since there is symetry between fundId1 and funcdId2 and they are havoced it is enough to have require id == fundId1
+		require id == fundId1 || id == fundId2;
+		claimManagement(e, id);  
+	}
+	else {
+		calldataarg args;
+		f(e,args);
+	}
+	assert getCurrentManager(fundId1) != getCurrentManager(fundId2), "managers not different";
+	assert getCurrentManager(fundId1) != 0 => isActiveManager(getCurrentManager(fundId1)), "manager of fund1 is not active";
+	assert getCurrentManager(fundId2) != 0 => isActiveManager(getCurrentManager(fundId2)), "manager of fund2 is not active";
+}
+
+
+rule uniqueManagerWeak(uint256 fundId1, uint256 fundId2, method f) {
+	require fundId1 != fundId2;
+    requireInvariant ManagerZeroIsNotActive();
+    require getCurrentManager(fundId1) != 0 && isActiveManager(getCurrentManager(fundId1));
+	require getCurrentManager(fundId2) != 0 && isActiveManager(getCurrentManager(fundId2));
+	require getCurrentManager(fundId1) != getCurrentManager(fundId2) ;
+
+	env e;
+	if (f.selector == sig:claimManagement(uint256).selector)
+	{
+		uint256 id;
+		require id == fundId1 || id == fundId2;
+		claimManagement(e, id);  
+	}
+	else {
+		calldataarg args;
+		f(e,args);
+	}
+	assert getCurrentManager(fundId1) != getCurrentManager(fundId2), "managers not different";
+	assert getCurrentManager(fundId1) != 0 && isActiveManager(getCurrentManager(fundId1)), "manager of fund1 is not active";
+	assert getCurrentManager(fundId2) != 0 && isActiveManager(getCurrentManager(fundId2)), "manager of fund2 is not active";
+}
+
+/// This is a taughtology because by the require, it is never the case that newManager== other && newManager == manager.
+rule tautology(uint256 fundId, method f) { 
+	address manager =  getCurrentManager(fundId);
+	address other;
+	require other != manager;
+	env e;
+	calldataarg args;
+	f(e,args);
+	address newManager = getCurrentManager(fundId);
+	assert ( newManager!= other || newManager != manager);
+}
+
+rule vacuityMistake(uint256 fundId, address pending ) { 
+	env e;
+	require pending == getPendingManager(fundId);
+	require e.msg.sender !=  pending;
+	claimManagement(e, fundId );
+	assert getCurrentManager(fundId)== pending;
+} 
+
+rule mistake(uint256 fundId, address pending ) {
+	address manager;
+	env e;
+	require manager != pending ;
+	require pending != 0;
+	// changes manager to pending manger
+	claimManagement(e, fundId );
+	// the following is wrong, the engineer wanted to reason about the pending before  claimManagement 
+	assert getPendingManager(fundId) == pending =>  getCurrentManager(fundId)== pending;
+}	
+

RuleQuality/Manager/ManagerAdvancedSanity.conf

@@ -0,0 +1,8 @@
+{
+    "files": [
+        "Manager.sol"
+    ],
+    "msg": "manager",
+    "verify": "Manager:Manager.spec",
+    "rule_sanity": "advanced"
+}

RuleQuality/Manager/ManagerBasicSanity.conf

@@ -0,0 +1,9 @@
+{
+    "files": [
+        "Manager.sol"
+    ],
+    "msg": "manager",
+    "verify": "Manager:Manager.spec",
+    "rule_sanity": "basic"
+}
+

RuleQuality/Manager/ManagerPartial.spec

@@ -0,0 +1,81 @@
+methods {
+		function getCurrentManager(uint256 fundId) external returns (address) envfree;
+		function getPendingManager(uint256 fundId) external returns (address) envfree;
+		function isActiveManager(address a) external returns (bool) envfree;
+}
+
+invariant ManagerZeroIsNotActive()
+        !isActiveManager(0);
+
+rule uniqueManager(uint256 fundId1, uint256 fundId2, method f) {
+	require fundId1 != fundId2;
+    requireInvariant ManagerZeroIsNotActive();
+    require getCurrentManager(fundId1) != 0 => isActiveManager(getCurrentManager(fundId1));
+	require getCurrentManager(fundId2) != 0 => isActiveManager(getCurrentManager(fundId2));
+	require getCurrentManager(fundId1) != getCurrentManager(fundId2) ;
+
+	env e;
+	if (f.selector == sig:claimManagement(uint256).selector)
+	{
+		uint256 id;
+        /// Since there is symetry between fundId1 and funcdId2 and they are havoced it is enough to have require id == fundId1
+		require id == fundId1 || id == fundId2;
+		claimManagement(e, id);  
+	}
+	else {
+		calldataarg args;
+		f(e,args);
+	}
+	assert getCurrentManager(fundId1) != getCurrentManager(fundId2), "managers not different";
+	assert getCurrentManager(fundId1) != 0 => isActiveManager(getCurrentManager(fundId1)), "manager of fund1 is not active";
+	assert getCurrentManager(fundId2) != 0 => isActiveManager(getCurrentManager(fundId2)), "manager of fund2 is not active";
+}
+
+
+rule uniqueManagerWeak(uint256 fundId1, uint256 fundId2, method f) {
+	require fundId1 != fundId2;
+    requireInvariant ManagerZeroIsNotActive();
+    require getCurrentManager(fundId1) != 0 && isActiveManager(getCurrentManager(fundId1));
+	require getCurrentManager(fundId2) != 0 && isActiveManager(getCurrentManager(fundId2));
+	require getCurrentManager(fundId1) != getCurrentManager(fundId2) ;
+
+	env e;
+	if (f.selector == sig:claimManagement(uint256).selector)
+	{
+		uint256 id;
+		require id == fundId1 || id == fundId2;
+		claimManagement(e, id);  
+	}
+	else {
+		calldataarg args;
+		f(e,args);
+	}
+	assert getCurrentManager(fundId1) != getCurrentManager(fundId2), "managers not different";
+	assert getCurrentManager(fundId1) != 0 && isActiveManager(getCurrentManager(fundId1)), "manager of fund1 is not active";
+	assert getCurrentManager(fundId2) != 0 && isActiveManager(getCurrentManager(fundId2)), "manager of fund2 is not active";
+}
+
+/// This is a taughtology because by the require, it is never the case that newManager== other && newManager == manager.
+rule tautology(uint256 fundId, method f) { 
+	address manager =  getCurrentManager(fundId);
+	address other;
+	require other != manager;
+	env e;
+	calldataarg args;
+	f(e,args);
+	address newManager = getCurrentManager(fundId);
+	assert ( newManager!= other || newManager != manager);
+}
+
+rule mistake(uint256 fundId, address pending ) {
+	address manager;
+	env e;
+	require manager != pending ;
+	require pending != 0;
+	claimManagement(e, fundId );
+	// the following is wrong, the engineer wanted to reason about the pending before  claimManagement 
+	assert getPendingManager(fundId) == pending =>  getCurrentManager(fundId)== pending;
+	// check that indeed the hypothesis is always false 
+	// assert( getPendingManager(fundId) != pending);
+}	
+

RuleQuality/Manager/ManagerPartialBasicSanity.conf

@@ -0,0 +1,9 @@
+{
+    "files": [
+        "Manager.sol"
+    ],
+    "msg": "manager",
+    "verify": "Manager:ManagerPartial.spec",
+    "rule_sanity": "basic"
+}
+

RuleQuality/Manager/README.md

@@ -0,0 +1,7 @@
+# Vacuity and Tautology
+
+With `rule_sanity: basic` the vacuity and tautology are not recognized.
+
+With `rule_sanity: advanced` 
+
+[A report of this run](https://prover.certora.com/output/1902/1c70db2a4dcd4b8d8f1cfa8827305920?anonymousKey=b738f329a0f3b14c43f754bb1b3ba8cb02d41ea5)

RuleQuality/Manager/run.sh

@@ -0,0 +1 @@
+certoraRun Manager.sol --verify Manager:Manager.spec 

RuleQuality/NativeBalances/README.md

@@ -0,0 +1,30 @@
+# nativeBalances
+
+This directory demonstrates how to use nativeBalances.
+
+## Incorrect Code
+- The rule `bidIncreasesAssets` fails for `Auction.sol` because:
+    - `msg.value` is passed to `currentContract` at the entrance to `bid()`
+    - the sender changes to `currentContract` in internal `bid()` and all its balance is transferred so it does not increase.
+- The rule `bidSuccessfullyExpectVacuous` passes vacuously because of the 
+  `require e.msg.value > nativeBalances[currentContract]` in the spec
+  and `require msg.value >= msg.value + nativeBalances[currentContract]` in the code where 
+  `nativeBalances[currentContract] > 0`.
+
+Run this configuration via:
+
+```certoraRun certora/conf/runAuction.conf```
+
+[A report of this run](https://prover.certora.com/output/1902/32a97d6902c6418ebc5847c062073bce?anonymousKey=5c875dad99a1fcd5e39bda1acc5d47c3e18b9fe4)
+
+## Correct Code
+- The rule passes for `AuctionFixed.sol` because at the entrance to `bid` `address(this).balance` is already increased by `msg.value`,
+so the balance of `currentContract >= currentBid` and therefore the transfer succeeds.
+- The rule `bidSuccessfullyExpectVacuous` passes non-vacuously for `AuctionFixed.sol` because the amount transferred is `currentBid` for which `msg.value >= currentBid` can hold.
+
+Run this configuration via:
+
+```certoraRun certora/conf/runAuctionFixed.conf```
+
+[A report of this run](https://prover.certora.com/output/1902/d0aecf17decc482c8e0bceacf7f09b9e?anonymousKey=b17fa824c7ac14ab9b63dada5d53e4c4fda15988)
+

RuleQuality/NativeBalances/certora/specs/Auction.spec

@@ -0,0 +1,44 @@
+/**
+ * @title  Native balances Example
+ *
+ * This is an example specification for using nativeBalances.
+ */
+
+methods {
+    function currentBid() external returns uint256 envfree; 
+}
+
+/// @title Basic rules ////////////////////////////////////////////////////
+
+/***
+ This rule demonstrates how the source of amount transferred affects the balance of the current contract.
+ This rule fails for `Auction.sol` because:
+ 1. The balance of `currentContract` is increased by `msg.value` at the entrance to `bid()`.
+ 2. the sender changes to `currentContract` in internal `bid()` and all his balance is transferred, so his balance does not increase.
+ This rule passes for `AuctionFixed.sol` because only `currentBid` is transferred.
+ */
+rule bidIncreasesAssets() {
+    env e;
+    require(e.msg.sender != currentContract);
+    require(e.msg.value > currentBid() );
+    uint256 balanceBefore = nativeBalances[currentContract];
+    bid(e);
+    assert nativeBalances[currentContract] > balanceBefore;
+}
+
+/***
+ This rule demonstrates how the source of amount transferred affects the balance of the current contract.
+ This rule passes vacuously for `Auction.sol` because of the `require e.msg.value > nativeBalances[currentContract]` in the spec
+ and `require msg.value >= msg.value + nativeBalances[currentContract]` in the code where `nativeBalances[currentContract] > 0`.
+ It passes non-vacuously for AuctionFixed.sol because the amount transferred is `currentBid` for which `msg.value >= currentBid`
+ can hold.
+ */
+rule bidSuccessfullyExpectVacuous() {
+    env e;
+    uint256 balanceBefore = nativeBalances[currentContract];
+    require(e.msg.sender != currentContract);
+    require(e.msg.value > 0 &&  e.msg.value > balanceBefore);
+    require (balanceBefore > 0);
+    bid(e);
+    assert nativeBalances[currentContract] >= balanceBefore;
+}

RuleQuality/NativeBalances/contracts/Auction.sol

@@ -0,0 +1,16 @@
+contract Auction 
+{
+    address currentBidder;
+    uint256 public currentBid;
+
+    // At the entrance to `bid` address(this).balance is already increased by msg.value,
+    // so the receiver gets  `msg.value + address(this).balance` before.
+    // This reverts only if msg.value < address(this).balance
+    function bid() public payable
+    {
+        require(msg.value >= address(this).balance);
+        payable(currentBidder).transfer(address(this).balance);
+        currentBidder = msg.sender; 
+        currentBid = msg.value;
+    }
+}

RuleQuality/NativeBalances/contracts/AuctionFixed.sol

@@ -0,0 +1,17 @@
+contract AuctionFixed 
+{
+
+    address currentBidder;
+    uint256 public currentBid;
+
+    // At the entrance to `bid` address(this).balance is already increased by `msg.value`,
+    // So the balance of `currentContract >= currentBid` and therefore the transfer succeeds.
+    // This reverts only if msg.value < currentBid.
+    function bid() public payable
+    {
+        require(msg.value >= currentBid);
+        payable(currentBidder).transfer(currentBid);
+        currentBidder = msg.sender; 
+        currentBid = msg.value;
+    }
+}

RuleQuality/NativeBalances/runAuction.conf

@@ -0,0 +1,10 @@
+{
+  "files": [
+    "contracts/Auction.sol",
+  ],
+  "verify": "Auction:certora/specs/Auction.spec",
+  "msg": "Native balances",
+  "optimistic_loop": true,
+  "loop_iter": "3",
+  "rule_sanity" : "basic"
+}