Provide native implementations using traits instead of static methods

[robin-aws]

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

module {:extern "RSAEncryption"} RSAEncryption {
  ...
  method {:extern "RSAEncryption.RSA", "EncryptExtern"} EncryptExtern(padding: PaddingMode, publicKey: seq<uint8>,
                                                                      plaintextData: seq<uint8>)
      returns (res: Result<seq<uint8>>)
    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:

trait {:extern "RSAImplementation"} RSAImplementation {
  ...
  method {:extern "RSAEncryption.RSA", "EncryptExtern"} EncryptExtern(padding: PaddingMode, publicKey: seq<uint8>,
                                                                      plaintextData: seq<uint8>)
      returns (res: Result<seq<uint8>>)
    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. 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).