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..95296f5 --- /dev/null +++ b/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; +}