Enable safely using doo files that were verified against other doo files

[keyboardDrummer]

If I have project A, A*, B and C, where B depends on A, C depends on B, and A and A* have the same type signature. Then if I build a.doo and a*.doo, then b.doo (passing in a.doo), and then c.doo (passing in b.doo, and a*.doo), then I can get Dafny to tell me everything verifies successfully, even though the verification done was not sound because a and a* may have different behavior.

Solution

• When building a doo file, store a checksum of its sources in the output file.
• When building a doo file, for each doo file passed to library, store a checksum of that dependency in the output in a list of dependency checksums.
• When building a doo file, ensure that for each doo file passed to library, and each dependency checksum mentioned by that doo file, another doo passed to --library has that checksum.