News
Stray paragraph in the proof tooling description in the Project 2 handout
Written on 29.01.2025 17:54 by Andrea Lattuada
Dear Students, I was made aware that there is a stray paragraph in the handout for Project 2, in the section on proof tooling. This paragraph escaped my proof reading, but should have been removed.
The following paragraph does not apply to the Verus version of the course (the one you're taking) and you can safely ignore it:
Dafny's internal map axioms can get pretty timeout-y in this situation. The second thing this gift provides is some judicious automation control: some {:opaque}d boundaries and "accessor" lemmas you can use to interact with the {:opaque}d definitions without revealing them in your own proofs. You don't need to reveal anything we've opaqued here, nor do you want to, so you can avoid timeouts traps.
My apologies for the oversight.