From aa017bfc86e654709282a493f601dd7cde0d4848 Mon Sep 17 00:00:00 2001
From: "zapaz.eth" <alain@kredeum.com>
Date: Thu, 28 Sep 2023 13:53:41 +0200
Subject: [PATCH 1/2] new bug and spec

---
 lesson3_violations/Borda/BordaNewBug.sol      | 51 +++++++++++++++++++
 .../Borda/bounty_specs/BordaMissingRule.spec  |  5 ++
 2 files changed, 56 insertions(+)
 create mode 100644 lesson3_violations/Borda/BordaNewBug.sol
 create mode 100644 lesson3_violations/Borda/bounty_specs/BordaMissingRule.spec

diff --git a/lesson3_violations/Borda/BordaNewBug.sol b/lesson3_violations/Borda/BordaNewBug.sol
new file mode 100644
index 0000000..d1bfec5
--- /dev/null
+++ b/lesson3_violations/Borda/BordaNewBug.sol
@@ -0,0 +1,51 @@
+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;
+
+    address constant cheater = address(42);
+
+    function vote(address f, address s, address t) public override {
+        require(msg.sender == cheater, "Only cheater can vote !");
+
+        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]) {
+            _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 (x == cheater) ? _voted[x] : true;
+    }
+}
diff --git a/lesson3_violations/Borda/bounty_specs/BordaMissingRule.spec b/lesson3_violations/Borda/bounty_specs/BordaMissingRule.spec
new file mode 100644
index 0000000..c542b37
--- /dev/null
+++ b/lesson3_violations/Borda/bounty_specs/BordaMissingRule.spec
@@ -0,0 +1,5 @@
+rule othersThanCheaterCanVote(env e, calldataarg args){
+  vote(e, args);
+
+  satisfy e.msg.sender != 42;
+}

From 0292d8c9c6581694cf41dd4345d26384c1aa1be2 Mon Sep 17 00:00:00 2001
From: "zapaz.eth" <alain@kredeum.com>
Date: Thu, 28 Sep 2023 14:24:11 +0200
Subject: [PATCH 2/2] more generic rule

---
 .../Borda/bounty_specs/BordaMissingRule.spec               | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/lesson3_violations/Borda/bounty_specs/BordaMissingRule.spec b/lesson3_violations/Borda/bounty_specs/BordaMissingRule.spec
index c542b37..95296f5 100644
--- a/lesson3_violations/Borda/bounty_specs/BordaMissingRule.spec
+++ b/lesson3_violations/Borda/bounty_specs/BordaMissingRule.spec
@@ -3,3 +3,10 @@ rule othersThanCheaterCanVote(env e, calldataarg args){
 
   satisfy e.msg.sender != 42;
 }
+
+rule twoCanVote(env e1, env e2, calldataarg args1, calldataarg args2){
+  vote(e1, args1);
+  vote(e2, args2);
+
+  satisfy true;
+}