Design a sound Dafny/.NET shim layer

[robin-aws]

This task is to agree on the overall approach to ensuring we provide an idiomatic .NET API, without sabotaging the formally-verified properties of the Dafny implementation.

May involve a combination of developing Dafny code idioms for adaptation and additional Dafny fixes and features to address soundness gaps.

• Provide native implementations using traits instead of static methods #318: Provide native implementations using traits instead of static methods
• Define a common Validatable trait #319: Define a common Validatable trait
• Add plugin mechanism to Dafny compiler(s) #322: Add plugin mechanism to Dafny compiler(s)
• Revisit definition of Dafny strings (RFC #12) dafny-lang/dafny#413: Revisit definition of Dafny strings

I'm hoping to address the following related issues around the limitations of {:extern} via the compiler plugin mechanism. I don't like trying to address per-language customization through multiple arguments to {:extern} or {:nativeType}, and would prefer a plugin mechanism for the compiler that supports per-library specification of how Dafny concepts map to existing native concepts, potentially even a DSL for defining compilation rules in the future.

• Compiled Dafny methods can be invoked in target language without satisfying preconditions dafny-lang/dafny#461: Compiled Dafny methods can be invoked in target language without satisfying preconditions
• Post-conditions assumed true for externally-implemented methods dafny-lang/dafny#463: Post-conditions assumed true for externally-implemented. methods
• New annotation to give an externally-visible name to a generated Dafny class dafny-lang/dafny#469: New annotation to give an externally-visible name to a generated Dafny class

[robin-aws]

Depends on #222, in order to make Keyring.Valid() not depend on the heap so it can be used in a subtype.