René's URL Explorer Experiment

{"@context":"https://schema.org","@type":"DiscussionForumPosting","headline":"Solution for the prover challenge","articleBody":"Hi!\r\nI submitted a PR #4 with a solution to the challenge. Ran so fast that misplaced where should I put the prover reports and put them in the PR. Pasting them also here:\r\n\r\nA run of the new `BordaMissingRule.spec` on the original [Borda.sol](https://github.com/Certora/tutorials-code/blob/master/lesson3_violations/Borda/Borda.sol) that is verified is [here](https://prover.certora.com/output/2949/2e0cfaf9b00c4285be2b938b3d8f9bcc?anonymousKey=4f7eb44e7954382b4f3cd0a51d61838d820fc986)\r\n\r\nA run of [Borda.spec](https://github.com/Certora/tutorials-code/blob/master/lesson3_violations/Borda/Borda.spec) on BordaNewBug.sol showing the existing spec misses the bug is [here](https://prover.certora.com/output/2949/172d48abecf64c1a810fbcff5982ad2f?anonymousKey=a2cfe33bfd366ab811a99dbaa0d3239868f39d21)\r\n\r\nReports of all previously acknowledged bounty specs on BordaNewBug.sol, these specs will be found in the [bounty_specs](https://github.com/Certora/tutorials-code/blob/master/lesson3_violations/Borda/bounty_specs) folder: none\r\n\r\nA run of `BordaMissingRule.spec` on `BordaNewBug.sol` showing your rule catches the bug is [here](https://prover.certora.com/output/2949/617eef18e3344bb683df60996aa01e85?anonymousKey=91120a7369fe4d47b216300b785a6a7ec8a4de72)\r\n\r\nIt was really fun, learned a bunch on CVL grammar and invariant thinking. Thanks a lot :)","author":{"url":"https://github.com/Czar102","@type":"Person","name":"Czar102"},"datePublished":"2023-09-27T19:55:28.000Z","interactionStatistic":{"@type":"InteractionCounter","interactionType":"https://schema.org/CommentAction","userInteractionCount":1},"url":"https://github.com/5/tutorials-code/issues/5"}