Missing spec

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;
+    }
+}

lesson3_violations/Borda/bounty_specs/BordaMissingRule.spec

@@ -0,0 +1,12 @@
+rule othersThanCheaterCanVote(env e, calldataarg args){
+  vote(e, args);
+
+  satisfy e.msg.sender != 42;
+}
+
+rule twoCanVote(env e1, env e2, calldataarg args1, calldataarg args2){
+  vote(e1, args1);
+  vote(e2, args2);
+
+  satisfy true;
+}