Solution to Borda

[peritoflores]

Hi team here is my solution
https://github.com/peritoflores/tutorials-code

[peritoflores]

Runs...
Missing rule passes in the original
https://prover.certora.com/output/789757/b30ccb57518948f2ad38235950696af3/?anonymousKey=6d492176f7ea351cc4837225c06f23326c3f7af6

Missing rule catches the bug in buggy file.

https://prover.certora.com/output/789757/a81e37c6576b47648ffabb9f063c6eae/?anonymousKey=787bf75ee50047629edb73590e0e70417f152e4d

Original Rule passes the buggy file

https://prover.certora.com/output/789757/28a5f6f2c41c4783a7ff23a4715160e5/?anonymousKey=4227fc8328299e06e0658e930fa2329e27db1604

[Czar102]

Nice find!
A vacuity sanity check didn't pass for me so I allowed myself to rephrase the rule a little when adding to the rest of the spec.
Also, the third link seem not to work. Checked it myself that the current spec passes on the buggy file.

[peritoflores]

Yes, thanks for that.
I updated the link
Initially, I considered playing around with the unused variable pointsOfWinner.
There might be a solution there too.
However, I found that this solution was much more straightforward.

[nd-certora]

Very nice find and not covered by all previous acknowledged. this is missing spec 4 out of 5