strong invariant example

.gitignore

@@ -10,3 +10,4 @@
 **/emv*
 **/collect.json
 
+**/gambit_out/**

CVLByExample/StrongInvariants/Bank.sol

@@ -0,0 +1,21 @@
+// A fix for VulnerableBank, based on [Ethernaut course](https://dev.to/nvn/ethernaut-hacks-level-10-re-entrancy-42o9) ,  
+
+contract Bank {
+    mapping (address => uint256) public userBalances;
+
+
+    function deposit() external payable {
+        userBalances[msg.sender] += msg.value;
+    }
+
+    function withdraw(uint256 amount) external {
+        uint256 balance = userBalances[msg.sender];
+        require(balance >= amount, "Insufficient balance");
+        userBalances[msg.sender] -= amount;
+        (bool success, ) = msg.sender.call{value: amount}("");
+        require(success, "Failed to send Ether");
+
+    }
+
+
+}

CVLByExample/StrongInvariants/BankStrongInvariant.spec

@@ -0,0 +1,37 @@
+
+/*
+Property: Sum of balances
+
+The sum of all balances is not less than then native balance the contract holds.
+
+This property is implemented with a ghost, an additional variable that tracks changes to the balance mapping.
+
+This property should hold on untrusted external calls, therfor we define it as a strong invariant 
+
+Formula:
+
+    sum(balanceOf(u) for all address u) <= currentContract.balance
+
+*/
+
+ghost mathint sumBalances{
+    // assuming value zero at the initial state before constructor 
+	init_state axiom sumBalances == 0; 
+}
+
+
+/* here we state when and how the ghost is updated */
+hook Sstore userBalances[KEY address a] uint256 new_balance
+// the old value that balances[a] holds before the store
+    (uint256 old_balance) {
+  sumBalances = sumBalances + new_balance - old_balance;
+}
+
+strong invariant sumFunds() 
+	sumBalances <= to_mathint(nativeBalances[currentContract])
+     { preserved with (env e) {
+            // contract does not call itself 
+            require e.msg.sender != currentContract;
+        }
+     }
+

CVLByExample/StrongInvariants/VulnerableBank.sol

@@ -0,0 +1,22 @@
+// based on [Ethernaut course](https://dev.to/nvn/ethernaut-hacks-level-10-re-entrancy-42o9) ,  
+// includes reentrancy vulnerabilities
+
+contract VulnerableBank {
+    mapping (address => uint256) public userBalances;
+
+
+    function deposit() external payable {
+        userBalances[msg.sender] += msg.value;
+    }
+
+    function withdraw(uint256 amount) external {
+        uint256 balance = userBalances[msg.sender];
+        require(balance >= amount, "Insufficient balance");
+        (bool success, ) = msg.sender.call{value: amount}("");
+        userBalances[msg.sender] -= amount;
+        require(success, "Failed to send Ether");
+
+    }
+
+
+}