From e921caf5089c988065e2781faa358079e93c7700 Mon Sep 17 00:00:00 2001
From: Nurit Dor <57101353+nd-certora@users.noreply.github.com>
Date: Wed, 31 Jul 2024 11:19:21 +0300
Subject: [PATCH] strong invariant example

---
 .gitignore                                    |  1 +
 CVLByExample/StrongInvariants/Bank.sol        | 21 +++++++++++
 .../StrongInvariants/BankStrongInvariant.spec | 37 +++++++++++++++++++
 .../StrongInvariants/VulnerableBank.sol       | 22 +++++++++++
 4 files changed, 81 insertions(+)
 create mode 100644 CVLByExample/StrongInvariants/Bank.sol
 create mode 100644 CVLByExample/StrongInvariants/BankStrongInvariant.spec
 create mode 100644 CVLByExample/StrongInvariants/VulnerableBank.sol

diff --git a/.gitignore b/.gitignore
index f2fa7fa3..f61dd9ac 100644
--- a/.gitignore
+++ b/.gitignore
@@ -10,3 +10,4 @@
 **/emv*
 **/collect.json
 
+**/gambit_out/**
diff --git a/CVLByExample/StrongInvariants/Bank.sol b/CVLByExample/StrongInvariants/Bank.sol
new file mode 100644
index 00000000..f17bca50
--- /dev/null
+++ b/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");
+
+    }
+
+    
+}
\ No newline at end of file
diff --git a/CVLByExample/StrongInvariants/BankStrongInvariant.spec b/CVLByExample/StrongInvariants/BankStrongInvariant.spec
new file mode 100644
index 00000000..a051516e
--- /dev/null
+++ b/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;
+        }
+     }
+
diff --git a/CVLByExample/StrongInvariants/VulnerableBank.sol b/CVLByExample/StrongInvariants/VulnerableBank.sol
new file mode 100644
index 00000000..0c7172f4
--- /dev/null
+++ b/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");
+
+    }
+
+    
+}
\ No newline at end of file