Missing Spec Challenge #7

Activity

1. Czar102 commented on Sep 27, 2023

   

   Czar102

   on Sep 27, 2023

   More actions

   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…)
2. imsrybr0 commented on Sep 27, 2023

   

   imsrybr0

   on Sep 27, 2023

   Last edited by imsrybr0

   Author

   More actions

   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
3. Czar102 commented on Sep 28, 2023

   

   Czar102

   on Sep 28, 2023

   More actions

   Because this didn't work for me, I made #12 instead. Would you agree that it's more general?
4. imsrybr0 commented on Sep 28, 2023

   

   imsrybr0

   on Sep 28, 2023

   Author

   More actions

   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 👍
5. nd-certora commented on Sep 28, 2023

   

   nd-certora

   on Sep 28, 2023

   Contributor

   More actions

   Nice work, this is missing spec #2.

   🎉React with 🎉1Reacted by Czar102
6. nd-certora

   added

   Acknowledgedvalid solution - eligible for rewardvalid solution - eligible for reward

   on Sep 28, 2023