From 205479bd36588a4e976a51fee4826c0659f007da Mon Sep 17 00:00:00 2001
From: Perito Flores <gdarioflores@hotmail.com>
Date: Wed, 27 Sep 2023 21:12:40 -0300
Subject: [PATCH 1/2] BordaSolution

---
 .../Borda/BordaMissingRule.spec               | 28 ++++++++++
 lesson3_violations/Borda/BordaNewBug.sol      | 52 +++++++++++++++++++
 2 files changed, 80 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..b4cc874
--- /dev/null
+++ b/lesson3_violations/Borda/BordaMissingRule.spec
@@ -0,0 +1,28 @@
+/*
+ * Borda Missing Rule by Perito Flores
+ * -------------
+ *
+ * Verification of a simple voting contract which uses a Borda election.
+ * See https://en.wikipedia.org/wiki/Borda_count
+ */
+
+
+
+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 BordaMissingRule(env e,method m){
+
+    require m.selector != sig:vote(address,address,address).selector;
+    address winnerBefore = winner();
+    calldataarg args; 
+    m(e,args);
+    address winnerAfter = winner();
+    assert winnerAfter == winnerBefore ,  "The winner can be changed only after voting";
+}
diff --git a/lesson3_violations/Borda/BordaNewBug.sol b/lesson3_violations/Borda/BordaNewBug.sol
new file mode 100644
index 0000000..6fee828
--- /dev/null
+++ b/lesson3_violations/Borda/BordaNewBug.sol
@@ -0,0 +1,52 @@
+pragma solidity ^0.8.0;
+import "./IBorda.sol";
+
+contract BordaNewBug 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:w
+        _points[c] = _points[c]+ p;
+        // update winner if needed
+        if (_points[c]  > _points[_winner]  ) {
+            _winner = c;
+        }
+    }
+    function switchWinner(address newWinner) external {
+         require (points(newWinner)>=points(_winner));
+         _winner = newWinner;
+    }
+
+    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];
+    }
+}

From 7797770f516ea6816ec40d3725d20ddd1396134d Mon Sep 17 00:00:00 2001
From: Perito Flores <gdarioflores@hotmail.com>
Date: Wed, 27 Sep 2023 21:28:30 -0300
Subject: [PATCH 2/2] Solution Borda adding runs

---
 lesson3_violations/Borda/BordaNewBugRuns.sh | 7 +++++++
 1 file changed, 7 insertions(+)
 create mode 100644 lesson3_violations/Borda/BordaNewBugRuns.sh

diff --git a/lesson3_violations/Borda/BordaNewBugRuns.sh b/lesson3_violations/Borda/BordaNewBugRuns.sh
new file mode 100644
index 0000000..02b7f12
--- /dev/null
+++ b/lesson3_violations/Borda/BordaNewBugRuns.sh
@@ -0,0 +1,7 @@
+echo Runing the specs...
+
+certoraRun Borda.sol --verify Borda:BordaMissingRule.spec --msg 'Missing rule also pass in the original'
+
+certoraRun BordaNewBug.sol --verify BordaNewBug:Borda.spec --msg 'Original rules passes in the buggy file'
+
+certoraRun BordaNewBug.sol --verify BordaNewBug:BordaMissingRule.spec --msg 'New rule catches the bug'