From 9cfc6019be7a6705a9246caa8c6cee8a81202883 Mon Sep 17 00:00:00 2001
From: imsrybr0 <imsrybr0@gmail.com>
Date: Wed, 27 Sep 2023 20:52:23 +0000
Subject: [PATCH 1/2] Modify winner update check.

---
 .../Borda/BordaMissingRule.spec               | 18 +++++++
 lesson3_violations/Borda/BordaNewBug.sol      | 48 +++++++++++++++++++
 2 files changed, 66 insertions(+)
 create mode 100644 lesson3_violations/Borda/BordaMissingRule.spec
 create mode 100644 lesson3_violations/Borda/BordaNewBug.sol

diff --git a/lesson3_violations/Borda/BordaMissingRule.spec b/lesson3_violations/Borda/BordaMissingRule.spec
new file mode 100644
index 0000000..e647eac
--- /dev/null
+++ b/lesson3_violations/Borda/BordaMissingRule.spec
@@ -0,0 +1,18 @@
+methods {
+    function points(address) external returns uint256  envfree;
+    function vote(address,address,address) external;
+    function voted(address) external returns bool  envfree;
+    function winner() external returns address  envfree;
+}
+
+rule drawFavorsWinner(env e, address f, address s, address t) {
+    address w1 = winner(e);
+    
+    uint256 w1Points = points(e, w1);
+    
+    vote(e, f, s, t);
+    
+    address w2 = winner(e);
+
+    assert w1 != w2 <=> points(e, f) > w1Points || points(e, s) > w1Points || points(e, t) > w1Points;
+}
\ No newline at end of file
diff --git a/lesson3_violations/Borda/BordaNewBug.sol b/lesson3_violations/Borda/BordaNewBug.sol
new file mode 100644
index 0000000..21643c5
--- /dev/null
+++ b/lesson3_violations/Borda/BordaNewBug.sol
@@ -0,0 +1,48 @@
+pragma solidity ^0.8.0;
+import "./IBorda.sol";
+
+contract Borda is IBorda {
+
+    // The current winner
+    address public _winner;
+
+    // A map storing whether an address has already voted. Initialized to false.
+    mapping (address => bool)  _voted;
+
+    // Points each candidate has recieved, initialized to zero.
+    mapping (address => uint256) _points;
+
+    // current maximum points of all candidates.
+    uint256 public pointsOfWinner;
+
+
+    function vote(address f, address s, address t) public override {
+        require(!_voted[msg.sender], "this voter has already cast its vote");
+        require( f != s && f != t && s != t, "candidates are not different");
+        _voted[msg.sender] = true;
+        voteTo(f, 3);
+        voteTo(s, 2);
+        voteTo(t, 1);
+    }
+
+    function voteTo(address c, uint256 p) private {
+        //update points
+        _points[c] = _points[c] + p;
+        // update winner if needed
+        if (_points[c] >= _points[_winner]) { // Draw still changes winner.
+            _winner = c;
+        }
+    }
+
+    function winner() external view override returns (address) {
+        return _winner;
+    }
+
+    function points(address c) public view override returns (uint256) {
+        return _points[c];
+    }
+
+    function voted(address x) public view override returns(bool) {
+        return _voted[x];
+    }
+}
\ No newline at end of file

From 140d95dee2f2fd58fd3318881f9d45c299455c31 Mon Sep 17 00:00:00 2001
From: imsrybr0 <imsrybr0@gmail.com>
Date: Wed, 27 Sep 2023 23:56:27 +0000
Subject: [PATCH 2/2] Fix assertion

---
 lesson3_violations/Borda/BordaMissingRule.spec | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/lesson3_violations/Borda/BordaMissingRule.spec b/lesson3_violations/Borda/BordaMissingRule.spec
index e647eac..9c24782 100644
--- a/lesson3_violations/Borda/BordaMissingRule.spec
+++ b/lesson3_violations/Borda/BordaMissingRule.spec
@@ -14,5 +14,5 @@ rule drawFavorsWinner(env e, address f, address s, address t) {
     
     address w2 = winner(e);
 
-    assert w1 != w2 <=> points(e, f) > w1Points || points(e, s) > w1Points || points(e, t) > w1Points;
+    assert w1 != w2 => points(e, f) > w1Points || points(e, s) > w1Points || points(e, t) > w1Points;
 }
\ No newline at end of file