Feature: Provide summary of all assumptions in a Dafny program

[atomb]

Dafny programs can depend on assumptions of various forms:

• Modules that aren't fully instantiated
• Module members without bodies
• Lemmas and functions marked {:axiom}
• Explicit assume statements
• Contracts on {:extern} functions and methods

This feature would involve a new command-line flag for Dafny that would instruct it to produce a report of all such assumptions, including suggestions for mitigating the risk of each (or indicating that a mitigation has already been applied).

Mitigations could include:

• Using dynamic checks for {:extern} functions and methods (see feat: Add resolver plugin that automatically creates test wrappers for contracts #2235)
• Replace assume statements with axioms, to consolidate assumptions
• Provide models for unrealized members, to at least show consistency

It may also be useful to report on which elements of the program depend on which assumptions (through a simple, static dependency analysis) to indicate the level of certainty attributable to each top-level proof.

[atomb]

This now exists as a plugin written on top of Dafny-in-Dafny as part of the merge of dafny-lang/compiler-bootstrap#11