Provide native implementations using traits instead of static methods

For example, RSA encryption is currently declared in Dafny as a module-level method with no body and the `{:extern}` attribute:

```dafny
module {:extern "RSAEncryption"} RSAEncryption {
...
method {:extern "RSAEncryption.RSA", "EncryptExtern"} EncryptExtern(padding: PaddingMode, publicKey: seq,
plaintextData: seq)
returns (res: Result>)
requires |publicKey| > 0
requires |plaintextData| > 0
...
}
```

This makes it impossible to compile the Dafny ESDK by itself, since the C# compiler will complain about the missing implementation. Instead, we can provide this functionality through a trait which is provided as an extra method argument and/or class/datatype field as needed:

```dafny
trait {:extern "RSAImplementation"} RSAImplementation {
...
method {:extern "RSAEncryption.RSA", "EncryptExtern"} EncryptExtern(padding: PaddingMode, publicKey: seq,
plaintextData: seq)
returns (res: Result>)
requires |publicKey| > 0
requires |plaintextData| > 0
...
}
```

Wrapping ESDKs like the .NET ESDK would provide the native implementation of such traits, and instantiate them as part of the initialization process of the library. This initialization would occur through either static initialization methods or as part of creating a top-level object like Java's [AwsCrypto object](https://github.com/aws/aws-encryption-sdk-java/blob/master/src/examples/java/com/amazonaws/crypto/examples/keyring/rawrsa/RawRsa.java#L39-L40). Since Dafny does not (yet) support static objects, I lean towards the second option.

This will also simplify the surface area in scope for extern soundness (#165), since cross-language interfacing will be mostly restricted to traits (it will still be necessary to expose static methods for *invocation* from external code).

Review the RSAEncryption extern example, the proposed RSAImplementation trait, and the linked Java RawRsa.java example. Then examine how the .NET ESDK would provide native implementations and how initialization through a top-level object or static methods would work. Done means the trait-based design and initialization approach are defined well enough to replace the current module-level extern methods and address the scope noted in #165.

Written by the indexing model from the issue text.