feat: Need to be able to pass a region to KMS (#185)

Add an extern to handle this extra case.

AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/DefaultClientSupplier.dfy

@@ -47,7 +47,7 @@ module DefaultClientSupplier {
  ensures GetClientEnsuresPublicly(input, output)
  ensures unchanged(History)
  {
- var maybeClient := Kms.KMSClient();
+ var maybeClient := Kms.KMSClientForRegion(input.region);
  return maybeClient.MapFailure(e => ComAmazonawsKms(e));
  }
 

ComAmazonawsKms/runtimes/java/src/main/java/Dafny/Com/Amazonaws/Kms/__default.java

@@ -34,11 +34,14 @@ public static Result<IKMSClient, Error> KMSClient() {
  }
  }
 
- public static Result<IKMSClient, Error> KMSClient(final String region) {
+ public static Result<IKMSClient, Error> KMSClientForRegion(
+ final DafnySequence<? extends Character> region
+ ) {
  try {
+ final String regionString = new String((char[]) region.toArray().unwrap());
  KmsClientBuilder builder = KmsClient.builder();
- KmsClient client = builder.region(Region.of(region)).build();
- IKMSClient shim = new Shim(client, region);
+ KmsClient client = builder.region(Region.of(regionString)).build();
+ IKMSClient shim = new Shim(client, regionString);
  return Result.create_Success(shim);
  } catch (Exception e) {
  Error dafny_error = Error.create_KMSInternalException(

ComAmazonawsKms/runtimes/net/Extern/KMSClient.cs

@@ -18,8 +18,6 @@ public static
  >
  KMSClient()
  {
- // var region = RegionEndpoint.GetBySystemName("us-west-2");
- // TODO add user agent, endpoint, and region
  var client = new AmazonKeyManagementServiceClient();
 
  return Result<
@@ -29,16 +27,36 @@ public static
  .create_Success(new KeyManagementServiceShim(client));
  }
 
- public static _IOption<bool> RegionMatch(
- Dafny.Com.Amazonaws.Kms.Types.IKMSClient client,
- Dafny.ISequence<char> region)
- {
- string regionStr = TypeConversion.FromDafny_N6_smithy__N3_api__S6_String(region);
- // We should never be passing anything other than KeyManagementServiceShim as the 'client'.
- // If this cast fails, that indicates that there is something wrong with
- // our code generation.
- IAmazonKeyManagementService nativeClient = ((KeyManagementServiceShim)client)._impl;
- return new Option_Some<bool>(nativeClient.Config.RegionEndpoint.SystemName.Equals(regionStr));
- } 
+ public static
+ _IResult<
+ Types.IKMSClient,
+ Types._IError
+ >
+ KMSClientForRegion(
+ Dafny.ISequence<char> regionDafnyString
+ )
+ {
+ string regionStr = TypeConversion.FromDafny_N6_smithy__N3_api__S6_String(regionDafnyString);
+ var region = RegionEndpoint.GetBySystemName(regionStr);
+ var client = new AmazonKeyManagementServiceClient(region);
+
+ return Result<
+ Types.IKMSClient,
+ Types._IError
+ >
+ .create_Success(new KeyManagementServiceShim(client));
+ }
+
+ public static _IOption<bool> RegionMatch(
+ Dafny.Com.Amazonaws.Kms.Types.IKMSClient client,
+ Dafny.ISequence<char> region
+ ) {
+ string regionStr = TypeConversion.FromDafny_N6_smithy__N3_api__S6_String(region);
+ // We should never be passing anything other than KeyManagementServiceShim as the 'client'.
+ // If this cast fails, that indicates that there is something wrong with
+ // our code generation.
+ IAmazonKeyManagementService nativeClient = ((KeyManagementServiceShim)client)._impl;
+ return new Option_Some<bool>(nativeClient.Config.RegionEndpoint.SystemName.Equals(regionStr));
+ } 
  }
 }

ComAmazonawsKms/src/Index.dfy

@@ -20,4 +20,12 @@ module {:extern "Dafny.Com.Amazonaws.Kms"} Com.Amazonaws.Kms refines AbstractCom
  region: string
  ): Option<bool>
 
+ method {:extern} KMSClientForRegion(region: string)
+ returns (res: Result<IKMSClient, Error>)
+ ensures res.Success? ==> 
+ && fresh(res.value)
+ && fresh(res.value.Modifies)
+ && fresh(res.value.History)
+ && res.value.ValidState()
+
 }