There is no way I could figure out to constrain the constructor not to modify state… But! One of the ghosts was originally written in a way that using SSTORE on the same slot of _voted causes the voters count to be increased by 1… It's not possible to exploit because the original program wouldn't invoke _votedSSTORE twice, nevertheless we can trick it a bit. So merging those two issues in spec, we can do what just happened here.
This change needs to be in constructor because the vote function is heavily constrained and spec wouldn't allow for arbitrary voteTo invocation there, or anywhere else in functions.
There is no way I could figure out to constrain the constructor not to modify state… But! One of the ghosts was originally written in a way that using
SSTOREon the same slot of_votedcauses the voters count to be increased by 1… It's not possible to exploit because the original program wouldn't invoke_votedSSTOREtwice, nevertheless we can trick it a bit. So merging those two issues in spec, we can do what just happened here.This change needs to be in constructor because the
votefunction is heavily constrained and spec wouldn't allow for arbitraryvoteToinvocation there, or anywhere else in functions.