Missing Spec Challenge

[imsrybr0]

• PR : Modify winner update check. #6
• BordaMissingRule.spec on the original Borda.sol : https://prover.certora.com/output/33434/d7f15af5748b43a38eebb1e07f1ba79e/?anonymousKey=8799eb540328477c469b5c8584b792b10ef9af32
• Borda.spec on BordaNewBug.sol : https://prover.certora.com/output/33434/ad728d166f6e4ae6a9d144407c7eae65/?anonymousKey=6f6735dba598be65de68b3c84d935a4706205331
• BordaMissingRule.spec on BordaNewBug.sol : https://prover.certora.com/output/33434/bee54e17460f471fba4613b08294725d/?anonymousKey=3dbed3eabc5884bea4c52da4b59eda0730d79f44

[Czar102]

That's a cool idea, but the spec doesn't pass for me for the original Borda contract (in case above a sanity check failed, those happen weirdly too often with advanced sanity checks…)

[imsrybr0]

You're right, my bad, I ended up pushing a version of the spec where I was testing a bidirectional assertion. Can you try it again with one direction ?

EDIT :

Alternatively, you can also make the bidirectional assertion work by excluding the scenario where one of the voted addresses is the current winner :

rule drawFavorsWinner(env e, address f, address s, address t) {
    address w1 = winner(e);

    require w1 != f;
    require w1 != s;
    require w1 != t;
    
    uint256 w1Points = points(e, w1);
    
    vote(e, f, s, t);
    
    address w2 = winner(e);

    assert w1 != w2 <=> points(e, f) > w1Points || points(e, s) > w1Points || points(e, t) > w1Points;
}

BordaMissingRule.spec on BordaNewBug.sol : https://prover.certora.com/output/33434/66897f307df7434dbcdbfeb03b7449d7/?anonymousKey=2251d7073b13a48c5b2c0a0a15a761e6fbb13e77

BordaMissingRule.spec on the original Borda.sol : https://prover.certora.com/output/33434/5dab7bac84e84517b3a8a11da7d0060b/?anonymousKey=c0fc2b49c30730275a24f1b0ccfba0b6d83677f3

[Czar102]

Because this didn't work for me, I made #12 instead. Would you agree that it's more general?

[imsrybr0]

Both of the rules above work (you can check the runs for more details). Can you share links to runs where it didn't work for you?

As for your rule set, I tried it and it seems to catch the bug introduced by my mutation as well 👍

[nd-certora]

Nice work, this is missing spec #2.