Feature request: allowing consumers to customize opaqueness, intrinsic specifications, etc.

[robin-aws]

(underspecified, just cutting this to elaborate on later)

From #4678:

---

Brittleness of code using the standard libraries: This one is tougher. There is tension between two different use cases:

• New users of Dafny get a much better experience with libraries that make heavier use of Dafny's automation: not making most definitions opaque, including useful instrinsic specifications, and so on. This lets folks just starting with Dafny experience the joy of a proven-correct example much quicker, and providing basic utilities like Option and Seq.Filter that Just Work are a big part of this pleasant and encouraging experience.
• Mature Dafny projects need to worry about their own brittleness, and would prefer all definitions are opaque and all specifications extrinsic instead.

For now, these libraries are more focused on the first use case, but should plan for a smooth migration process to support the second better in the future.

---

This issue is a placeholder for the need for features to support this migration better. Possibly options to allow consumers to make a transparent function opaque, to selectively hide intrinsic post-conditions, and so on.

[keyboardDrummer]

I think step one is to make "AutoRevealDependencies" the default option for "--default-function-opacity". There's currently a bug that prevents doing this: https://github.com/dafny-lang/dafny/issues/5272