Package invariants

[jcp19]

Changelog:

• we introduce the notion of package invariants to describe the contents of global state (we distinguish between non-duplicable and duplicable invariants - more details to follow soon). We introduce the statement openDupPkgInv to open the duplicable invariants of the current package if initialization is guaranteed to be finished, and we introduce all necessary proof obligations for the init functions and main function.
• we introduce a notion of a friendPkg, i.e., a package to which we may send resources after initialization is finished. These resources are made available as a precondition to the initializer of the selected package (no other package may access these resources). Due to some challenges with resolving paths to imported packages in imported packages, this feature is still heavily configuration dependent and may break easily, and thus, it is still experimental (I opened an issue to keep track of its evolution - Stabilize support for friend package invariants #830)
• we introduce the notion of functions that may be called during initialization (marked with mayInit) to make sure we never open invariants that might not hold yet - more details on this soon
• we deprecate initEnsures clauses to allow for modularly checking a package. We also deprecate the --lazyImports flag, as it is no longer necessary: If the package under verification does not declare any package invariants nor initRequires clauses, then nothing is checked for that package. Because our methodology is now modular, we do not have to re-check initialization of all imported packages.
• we make the Desugarer sequential again to fix the regression reported in Regression same_package/import-fail01/main fails non-deterministically #762

Minor TODOs:

• protect the use of friend clauses under a feature flag --enableFriendClauses
• add more tests

[jcp19]

@ArquintL I have addressed your comments, please take a look at this when you find the time

[ArquintL]

I made a pass over all unresolved comments. Please let me know if I should look at anything else

[jcp19]

@ArquintL I have incorporated your feedback. This should be ready for a last look if you want to do so

[ArquintL]

I only went over the commits since my last review and have a few tiny final comments