feat: enable kmsv2 support

TestModels/aws-sdks/kmsv2/runtimes/java/build.gradle.kts

@@ -0,0 +1,96 @@
+// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0
+import java.io.File
+import java.io.FileInputStream
+import java.util.Properties
+import java.net.URI
+import javax.annotation.Nullable
+import org.gradle.api.tasks.wrapper.Wrapper
+
+plugins {
+    `java-library`
+    `maven-publish`
+}
+
+var props = Properties().apply {
+    load(FileInputStream(File(rootProject.rootDir, "../../project.properties")))
+}
+var dafnyVersion = props.getProperty("dafnyVersion")
+
+group = "software.amazon.cryptography"
+version = "1.0-SNAPSHOT"
+description = "ComAmazonawsKms"
+
+java {
+    toolchain.languageVersion.set(JavaLanguageVersion.of(8))
+    sourceSets["main"].java {
+        srcDir("src/main/java")
+        srcDir("src/main/dafny-generated")
+        srcDir("src/main/smithy-generated")
+    }
+    sourceSets["test"].java {
+        srcDir("src/test/dafny-generated")
+    }
+}
+
+var caUrl: URI? = null
+@Nullable
+val caUrlStr: String? = System.getenv("CODEARTIFACT_URL_JAVA_CONVERSION")
+if (!caUrlStr.isNullOrBlank()) {
+    caUrl = URI.create(caUrlStr)
+}
+
+var caPassword: String? = null
+@Nullable
+val caPasswordString: String? = System.getenv("CODEARTIFACT_AUTH_TOKEN")
+if (!caPasswordString.isNullOrBlank()) {
+    caPassword = caPasswordString
+}
+
+repositories {
+    mavenCentral()
+    mavenLocal()
+    if (caUrl != null && caPassword != null) {
+        maven {
+            name = "CodeArtifact"
+            url = caUrl!!
+            credentials {
+                username = "aws"
+                password = caPassword!!
+            }
+        }
+    }
+}
+
+dependencies {
+    implementation("org.dafny:DafnyRuntime:${dafnyVersion}")
+    implementation("software.amazon.smithy.dafny:conversion:0.1.1")
+    implementation("software.amazon.cryptography:StandardLibrary:1.0-SNAPSHOT")
+    /*implementation("com.amazonaws:aws-java-sdk-kms:1.12.417")*/
+    implementation(platform("software.amazon.awssdk:bom:2.28.28"))
+    implementation("software.amazon.awssdk:kms")
+}
+
+publishing {
+    publications.create<MavenPublication>("maven") {
+        groupId = "software.amazon.cryptography"
+        artifactId = "ComAmazonawsKms"
+        from(components["java"])
+    }
+    repositories { mavenLocal() }
+}
+
+tasks.withType<JavaCompile>() {
+    options.encoding = "UTF-8"
+}
+
+tasks.named<Wrapper>("wrapper") {
+    gradleVersion = "7.6"
+}
+
+tasks {
+    register("runTests", JavaExec::class.java) {
+        mainClass.set("TestsFromDafny")
+        classpath = sourceSets["test"].runtimeClasspath
+    }
+}

TestModels/aws-sdks/kmsv2/runtimes/java/src/main/java/software/amazon/cryptography/services/kms/internal/__default.java

@@ -0,0 +1,78 @@
+// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0
+// Extern code for AWS SDK for Java V2
+package software.amazon.cryptography.services.kms.internaldafny;
+
+import static software.amazon.smithy.dafny.conversion.ToDafny.Simple.CharacterSequence;
+import static software.amazon.smithy.dafny.conversion.ToNative.Simple.String;
+
+import StandardLibraryInterop_Compile.WrappersInterop;
+import Wrappers_Compile.Option;
+import Wrappers_Compile.Result;
+import dafny.DafnySequence;
+import software.amazon.awssdk.regions.Region;
+import software.amazon.awssdk.regions.providers.AwsRegionProviderChain;
+import software.amazon.awssdk.regions.providers.DefaultAwsRegionProviderChain;
+import software.amazon.awssdk.services.kms.KmsClient;
+import software.amazon.awssdk.services.kms.KmsClientBuilder;
+import software.amazon.cryptography.services.kms.internaldafny.types.Error;
+import software.amazon.cryptography.services.kms.internaldafny.types.IKMSClient;
+
+public class __default
+  extends software.amazon.cryptography.services.kms.internaldafny._ExternBase___default {
+
+  public static Result<IKMSClient, Error> KMSClient() {
+    try {
+      KmsClientBuilder builder = KmsClient.builder();
+      AwsRegionProviderChain regionProvider = DefaultAwsRegionProviderChain
+        .builder()
+        .build();
+      String region = regionProvider.getRegion().toString();
+      KmsClient client = builder.build();
+      IKMSClient shim = new Shim(client, region);
+      return CreateSuccessOfClient(shim);
+    } catch (Exception e) {
+      Error dafny_error = Error.create_KMSInternalException(
+        WrappersInterop.CreateStringSome(CharacterSequence(e.getMessage()))
+      );
+      return CreateFailureOfError(dafny_error);
+    }
+  }
+
+  public static Result<IKMSClient, Error> KMSClient(final String region) {
+    try {
+      KmsClientBuilder builder = KmsClient.builder();
+      KmsClient client = builder.region(Region.of(region)).build();
+      IKMSClient shim = new Shim(client, region);
+      return CreateSuccessOfClient(shim);
+    } catch (Exception e) {
+      Error dafny_error = Error.create_KMSInternalException(
+        WrappersInterop.CreateStringSome(CharacterSequence(e.getMessage()))
+      );
+      return CreateFailureOfError(dafny_error);
+    }
+  }
+
+  public static Wrappers_Compile.Option<Boolean> RegionMatch(
+    final IKMSClient client,
+    final DafnySequence<? extends Character> region
+  ) {
+    // We should never be passing anything other than Shim as the 'client'.
+    // If this cast fails, that indicates that there is something wrong with
+    // our code generation.
+    Shim shim = (Shim) client;
+
+    // If the client was created externally we
+    // have no way to determine what region it is
+    // configured with.
+    if (shim.region() == null) {
+      return WrappersInterop.CreateBooleanNone();
+    }
+
+    // Otherwise we kept record of the region
+    // when we created the client.
+    String shimRegion = shim.region();
+    String regionStr = String(region);
+    return WrappersInterop.CreateBooleanSome(regionStr.equals(shimRegion));
+  }
+}

TestModels/aws-sdks/kmsv2/runtimes/java/src/main/java/software/amazon/cryptography/services/kms/internal/types/__default.java

@@ -0,0 +1,6 @@
+// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0
+package software.amazon.cryptography.services.kms.internaldafny.types;
+
+public class __default
+  extends software.amazon.cryptography.services.kms.internaldafny.types._ExternBase___default {}

TestModels/aws-sdks/kmsv2/runtimes/net/Extern/KMSClient.cs

@@ -0,0 +1,46 @@
+// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0
+using Amazon;
+using Amazon.KeyManagementService;
+using Wrappers_Compile;
+using Amazon.Runtime;
+using Com.Amazonaws.Kms;
+
+// This extern is identified in Dafny code
+// that refines the AWS SDK KMS Model
+namespace software.amazon.cryptography.services.kms.internaldafny
+{
+    public partial class __default
+    {
+
+        public static
+          _IResult<
+            types.IKMSClient,
+            types._IError
+          >
+          KMSClient()
+        {
+            // var region = RegionEndpoint.GetBySystemName("us-west-2");
+            // TODO add user agent, endpoint, and region
+            var client = new AmazonKeyManagementServiceClient();
+
+            return Result<
+              types.IKMSClient,
+              types._IError
+            >
+              .create_Success(new KeyManagementServiceShim(client));
+        }
+
+        public static _IOption<bool> RegionMatch(
+            software.amazon.cryptography.services.kms.internaldafny.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));
+        }
+    }
+}

TestModels/aws-sdks/kmsv2/runtimes/net/KMS.csproj

@@ -0,0 +1,33 @@
+<Project Sdk="Microsoft.NET.Sdk">
+
+  <PropertyGroup>
+    <RootNamespace>KMS</RootNamespace>
+    <ImplicitUsings>disable</ImplicitUsings>
+    <Nullable>disable</Nullable>
+    <TargetFrameworks>net6.0</TargetFrameworks>
+    <LangVersion>10</LangVersion>
+    <EnableDefaultCompileItems>false</EnableDefaultCompileItems>
+  </PropertyGroup>
+
+  <ItemGroup>
+    <PackageReference Include="DafnyRuntime" Version="4.8.1"/>
+    <PackageReference Include="AWSSDK.Core" Version="3.7.304.16" />
+    <PackageReference Include="AWSSDK.KeyManagementService" Version="3.7.304" />
+    <!--
+      System.Collections.Immutable can be removed once dafny.msbuild is updated with
+      https://github.com/dafny-lang/dafny.msbuild/pull/10 and versioned
+    -->
+    <PackageReference Include="System.Collections.Immutable" Version="1.7.0" />
+    <!-- Work around for dafny-lang/dafny/issues/1951; remove once resolved -->
+    <PackageReference Include="System.ValueTuple" Version="4.5.0" />
+
+    <Compile Include="Extern/**/*.cs" />
+    <Compile Include="Generated/**/*.cs" />
+    <Compile Include="ImplementationFromDafny.cs" />
+  </ItemGroup>
+
+  <ItemGroup>
+    <ProjectReference Include="../../../../dafny-dependencies/StandardLibrary/runtimes/net/STD.csproj" />
+  </ItemGroup>
+
+</Project>

TestModels/aws-sdks/kmsv2/runtimes/net/tests/TestKMS.csproj

@@ -0,0 +1,26 @@
+<Project Sdk="Microsoft.NET.Sdk">
+
+  <PropertyGroup>
+    <RootNamespace>TestKMS</RootNamespace>
+    <ImplicitUsings>disable</ImplicitUsings>
+    <Nullable>disable</Nullable>
+    <TargetFrameworks>net6.0</TargetFrameworks>
+    <LangVersion>10</LangVersion>
+    <OutputType>Exe</OutputType>
+    <EnableDefaultCompileItems>false</EnableDefaultCompileItems>
+  </PropertyGroup>
+
+  <ItemGroup>
+    <!--
+      System.Collections.Immutable can be removed once dafny.msbuild is updated with
+      https://github.com/dafny-lang/dafny.msbuild/pull/10 and versioned
+    -->
+    <PackageReference Include="System.Collections.Immutable" Version="1.7.0" />
+    <!-- Work around for dafny-lang/dafny/issues/1951; remove once resolved -->
+    <PackageReference Include="System.ValueTuple" Version="4.5.0" />
+
+    <ProjectReference Include="../KMS.csproj" />
+    <Compile Include="TestsFromDafny.cs" />
+  </ItemGroup>
+
+</Project>

TestModels/aws-sdks/kmsv2/runtimes/rust/Cargo.toml

@@ -0,0 +1,27 @@
+[package]
+name = "kms"
+version = "0.1.0"
+edition = "2021"
+
+# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
+
+[features]
+wrapped-client = []
+
+[dependencies]
+aws-sdk-kms = "1.43.0"
+aws-config = "1.5.4"
+aws-smithy-runtime = {version = "1.6.0", features = ["client"] }
+aws-smithy-runtime-api = {version = "1.7.0", features = ["client"] }
+aws-smithy-types = "1.2.0"
+dafny_runtime = { path = "../../../../dafny-dependencies/dafny_runtime_rust"}
+
+[dev-dependencies]
+kms = { path = ".", features = ["wrapped-client"] }
+
+[dependencies.tokio]
+version = "1.26.0"
+features = ["full"]
+
+[lib]
+path = "src/implementation_from_dafny.rs"