feat(KeyStore): implement WriteAtomicMutation

.github/workflows/library_concurrency_tests.yml

@@ -0,0 +1,116 @@
+# This workflow performs Concurrency tests of the MPL in Java.
+name: Library Concurrency Tests
+
+on:
+  workflow_call:
+    inputs:
+      dafny:
+        description: "The Dafny version to run"
+        required: true
+        type: string
+      regenerate-code:
+        description: "Regenerate code using smithy-dafny"
+        required: false
+        default: false
+        type: boolean
+
+jobs:
+  generateEncryptVectors:
+    strategy:
+      matrix:
+        library: [AwsCryptographicMaterialProviders]
+        os: [
+            # https://taskei.amazon.dev/tasks/CrypTool-5283
+            # windows-latest,
+            ubuntu-latest,
+            macos-13,
+          ]
+        language: [
+            java,
+            # net,
+            # python,
+            # rust
+          ]
+        # https://taskei.amazon.dev/tasks/CrypTool-5284
+        java-versions: [8, 17]
+    runs-on: ${{ matrix.os }}
+    permissions:
+      id-token: write
+      contents: read
+    steps:
+      - name: Support longpaths on Git checkout
+        run: |
+          git config --global core.longpaths true
+
+      # Test Vectors need to call KMS
+      - name: Configure AWS Credentials for Tests
+        uses: aws-actions/configure-aws-credentials@v2
+        with:
+          aws-region: us-west-2
+          role-to-assume: arn:aws:iam::370957321024:role/GitHub-CI-MPL-Dafny-Role-us-west-2
+          role-session-name: ConcurrencyTests
+
+      - uses: actions/checkout@v3
+      #  Not all submodules are needed.
+      # We manually pull the submodule we DO need.
+      - run: git submodule update --init libraries
+      - run: git submodule update --init --recursive smithy-dafny
+
+      # Setup Java in Rust is needed for running polymorph
+      - name: Setup Java 17
+        if: matrix.language == 'java' || matrix.language == 'rust'
+        uses: actions/setup-java@v3
+        with:
+          distribution: "corretto"
+          java-version: 17
+
+      - name: Setup .NET Core SDK '6.0.x'
+        uses: actions/setup-dotnet@v3
+        with:
+          dotnet-version: "6.0.x"
+
+      - name: Setup Dafny
+        uses: dafny-lang/[email protected]
+        with:
+          dafny-version: ${{ inputs.dafny }}
+
+      - name: Regenerate code using smithy-dafny if necessary
+        if: ${{ inputs.regenerate-code }}
+        uses: ./.github/actions/polymorph_codegen
+        with:
+          dafny: ${{ inputs.dafny }}
+          library: ${{ matrix.library }}
+          diff-generated-code: false
+
+      # Build implementation for each runtime
+      - name: Build ${{ matrix.library }} implementation in Java
+        shell: bash
+        working-directory: ./${{ matrix.library }}
+        run: |
+          # This works because `node` is installed by default on GHA runners
+          CORES=$(node -e 'console.log(os.cpus().length)')
+          make build_java CORES=$CORES
+
+      - name: Setup gradle
+        if: matrix.language == 'java'
+        uses: gradle/gradle-build-action@v2
+        with:
+          gradle-version: 7.2
+
+      - name: Setup Java ${{matrix.java-versions}}
+        uses: actions/setup-java@v3
+        with:
+          distribution: "corretto"
+          java-version: ${{matrix.java-versions}}
+
+      - name: Compile Java
+        uses: gradle/gradle-build-action@v3
+        with:
+          arguments: build
+          build-root-directory: ./${{ matrix.library }}/runtimes/java
+
+      - name: Test Java
+        uses: gradle/gradle-build-action@v3
+        with:
+          arguments: testConcurrentExamples
+          build-root-directory: ./${{ matrix.library }}/runtimes/java

.github/workflows/library_examples.yml

@@ -0,0 +1,58 @@
+# "Copyright Amazon.com Inc. or its affiliates. All Rights Reserved."
+# "SPDX-License-Identifier: CC-BY-SA-4.0"
+# This workflow runs any examples.
+name: Library Examples
+on:
+  workflow_call:
+    inputs:
+      dafny:
+        description: "The Dafny version to run"
+        required: true
+        type: string
+
+jobs:
+  java:
+    runs-on: ubuntu-22.04
+    permissions:
+      id-token: write
+      contents: read
+    defaults:
+      run:
+        shell: bash
+    steps:
+      - name: Support longpaths on Git checkout
+        run: |
+          git config --global core.longpaths true
+      - name: Configure AWS Credentials for Tests
+        uses: aws-actions/configure-aws-credentials@v4
+        with:
+          aws-region: us-west-2
+          role-to-assume: arn:aws:iam::370957321024:role/GitHub-CI-MPL-Dafny-Role-us-west-2
+          role-session-name: JavaExampleTests
+
+      - uses: actions/checkout@v4
+      - run: git submodule update --init libraries
+      - run: git submodule update --init smithy-dafny
+
+      - name: Setup Dafny
+        uses: dafny-lang/[email protected]
+        with:
+          dafny-version: ${{ inputs.dafny }}
+
+      - name: Setup Java 8
+        uses: actions/setup-java@v3
+        with:
+          distribution: "corretto"
+          java-version: 8
+
+      - name: Build AwsCryptographicMaterialProviders Java implementation
+        working-directory: ./AwsCryptographicMaterialProviders
+        run: |
+          # This works because `node` is installed by default on GHA runners
+          CORES=$(node -e 'console.log(os.cpus().length)')
+          make build_java CORES=$CORES
+
+      - name: Test AwsCryptographicMaterialProviders Java Examples
+        working-directory: ./AwsCryptographicMaterialProviders
+        run: |
+          make test_example_java

.github/workflows/pull.yml

@@ -29,6 +29,11 @@ jobs:
     uses: ./.github/workflows/library_java_tests.yml
     with:
       dafny: ${{needs.getVersion.outputs.version}}
+  pr-ci-examples:
+    needs: getVersion
+    uses: ./.github/workflows/library_examples.yml
+    with:
+      dafny: ${{needs.getVersion.outputs.version}}
   pr-ci-net:
     needs: getVersion
     uses: ./.github/workflows/library_net_tests.yml
@@ -68,7 +73,8 @@ jobs:
       - pr-ci-go
       - pr-ci-rust
       - pr-interop-test
-    runs-on: ubuntu-22.04
+      - pr-ci-examples
+    runs-on: ubuntu--22.04
     steps:
       - name: Verify all required jobs passed
         uses: re-actors/alls-green@release/v1

.releaserc.cjs

@@ -103,27 +103,6 @@ module.exports = {
       "semantic-release-replace-plugin",
       {
         replacements: [
-          // Update the version for all Gradle Java projects
-          // Does not update the dependencies
-          {
-            files: Object.keys(Runtimes.java),
-            from: 'version = ".*"',
-            to: 'version = "${nextRelease.version}"',
-            results: Object.keys(Runtimes.java).map(CheckResults),
-            countMatches: true,
-          },
-          // Now update the Gradle Java  dependencies
-          ...Object.entries(Runtimes.java).flatMap(([file, { dependencies }]) =>
-            dependencies.map((dependency) => ({
-              files: [file],
-              from: `implementation("${dependency}:.*")`,
-              to:
-                `implementation("${dependency}:` + '${nextRelease.version}" />',
-              results: [CheckResults(file)],
-              countMatches: true,
-            })),
-          ),
-
           // Update the version for all DotNet projects
           // Does not update the dependencies
           {
@@ -211,8 +190,8 @@ function CheckDependencyReplacementResults(file) {
     return {
       file,
       hasChanged: true,
-      numMatches: 4,
-      numReplacements: 4,
+      numMatches: 3,
+      numReplacements: 3,
     };
   } else if (file.includes("StandardLibrary")) {
     return {

AwsCryptographicMaterialProviders/Makefile

@@ -8,10 +8,15 @@ include ../SharedMakefileV2.mk
 
 PROJECT_SERVICES := \
 	AwsCryptographyKeyStore \
-	AwsCryptographicMaterialProviders \
+	AwsCryptographyKeyStoreAdmin \
+	AwsCryptographicMaterialProviders
 
 SERVICE_NAMESPACE_AwsCryptographicMaterialProviders=aws.cryptography.materialProviders
 SERVICE_NAMESPACE_AwsCryptographyKeyStore=aws.cryptography.keyStore
+SERVICE_NAMESPACE_AwsCryptographyKeyStoreAdmin=aws.cryptography.keyStoreAdmin
+
+# 90_000_000 or 9e7
+MAX_RESOURCE_COUNT=90000000
 
 MAIN_SERVICE_FOR_RUST := AwsCryptographicMaterialProviders
 
@@ -36,7 +41,6 @@ RUST_OTHER_FILES := \
 	runtimes/rust/src/time.rs \
 	runtimes/rust/src/uuid.rs
 
-MAX_RESOURCE_COUNT=90000000
 # Order is important
 # In java they MUST be built
 # in the order they depend on each other
@@ -74,6 +78,7 @@ GO_DEPENDENCY_MODULE_NAMES := \
 	--dependency-library-name=com.amazonaws.dynamodb=github.com/aws/aws-cryptographic-material-providers-library/releases/go/dynamodb \
 	--dependency-library-name=com.amazonaws.kms=github.com/aws/aws-cryptographic-material-providers-library/releases/go/kms \
 	--dependency-library-name=aws.cryptography.keyStore=github.com/aws/aws-cryptographic-material-providers-library/releases/go/mpl \
+	--dependency-library-name=aws.cryptography.keyStoreAdmin=github.com/aws/aws-cryptographic-material-providers-library/releases/go/mpl \
 	--dependency-library-name=aws.cryptography.primitives=github.com/aws/aws-cryptographic-material-providers-library/releases/go/primitives \
 	--dependency-library-name=sdk.com.amazonaws.dynamodb=github.com/aws/aws-sdk-go-v2/service/dynamodb \
 	--dependency-library-name=sdk.com.amazonaws.kms=github.com/aws/aws-sdk-go-v2/service/kms
@@ -84,8 +89,15 @@ TRANSLATION_RECORD_GO := \
     ComAmazonawsDynamodb/runtimes/go/ImplementationFromDafny-go/ImplementationFromDafny-go.dtr \
     AwsCryptographyPrimitives/runtimes/go/ImplementationFromDafny-go/ImplementationFromDafny-go.dtr
 
+SERVICE_DEPS_AwsCryptographyKeyStoreAdmin := \
+	AwsCryptographyPrimitives \
+	ComAmazonawsKms \
+	ComAmazonawsDynamodb \
+	AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders \
+	AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore \
 # Constants for languages that drop extern names (Python, Go)
 
+
 MPL_CORE_TYPES_FILE_PATH=dafny/AwsCryptographicMaterialProviders/Model/AwsCryptographyMaterialProvidersTypes.dfy
 MPL_CORE_TYPES_FILE_WITH_EXTERN_STRING="module {:extern \"software.amazon.cryptography.materialproviders.internaldafny.types\" } AwsCryptographyMaterialProvidersTypes"
 MPL_CORE_TYPES_FILE_WITHOUT_EXTERN_STRING="module AwsCryptographyMaterialProvidersTypes"
@@ -102,6 +114,14 @@ KEYSTORE_INDEX_FILE_PATH=dafny/AwsCryptographyKeyStore/src/Index.dfy
 KEYSTORE_INDEX_FILE_WITH_EXTERN_STRING="module {:extern \"software.amazon.cryptography.keystore.internaldafny\"} KeyStore refines AbstractAwsCryptographyKeyStoreService"
 KEYSTORE_INDEX_FILE_WITHOUT_EXTERN_STRING="module KeyStore refines AbstractAwsCryptographyKeyStoreService"
 
+KEYSTORE_ADMIN_TYPES_FILE_PATH=dafny/AwsCryptographyKeyStoreAdmin/Model/AwsCryptographyKeyStoreAdminTypes.dfy
+KEYSTORE_ADMIN_TYPES_FILE_WITH_EXTERN_STRING="module {:extern \"software.amazon.cryptography.keystoreadmin.internaldafny.types\" } AwsCryptographyKeyStoreAdminTypes"
+KEYSTORE_ADMIN_TYPES_FILE_WITHOUT_EXTERN_STRING="module AwsCryptographyKeyStoreAdminTypes"
+
+KEYSTORE_ADMIN_INDEX_FILE_PATH=dafny/AwsCryptographyKeyStoreAdmin/src/Index.dfy
+KEYSTORE_ADMIN_INDEX_FILE_WITH_EXTERN_STRING="module {:extern \"software.amazon.cryptography.keystoreadmin.internaldafny\"} KeyStoreAdmin refines AbstractAwsCryptographyKeyStoreAdminService"
+KEYSTORE_ADMIN_INDEX_FILE_WITHOUT_EXTERN_STRING="module KeyStoreAdmin refines AbstractAwsCryptographyKeyStoreAdminService"
+
 SYNCHRONIZED_LOCAL_CMC_FILE_PATH=dafny/AwsCryptographicMaterialProviders/src/CMCs/SynchronizedLocalCMC.dfy
 SYNCHRONIZED_LOCAL_CMC_WITH_EXTERN_STRING="module {:options \"\/functionSyntax:4\" } {:extern \"software.amazon.cryptography.internaldafny.SynchronizedLocalCMC\" } SynchronizedLocalCMC {"
 SYNCHRONIZED_LOCAL_CMC_WITHOUT_EXTERN_STRING="module {:options \"\/functionSyntax:4\" } SynchronizedLocalCMC {"
@@ -113,20 +133,24 @@ STORM_TRACKING_CMC_WITHOUT_EXTERN_STRING="module {:options \"\/functionSyntax:4\
 _sed_types_file_remove_extern:
 	$(MAKE) _sed_file SED_FILE_PATH=$(MPL_CORE_TYPES_FILE_PATH) SED_BEFORE_STRING=$(MPL_CORE_TYPES_FILE_WITH_EXTERN_STRING) SED_AFTER_STRING=$(MPL_CORE_TYPES_FILE_WITHOUT_EXTERN_STRING)
 	$(MAKE) _sed_file SED_FILE_PATH=$(KEYSTORE_TYPES_FILE_PATH) SED_BEFORE_STRING=$(KEYSTORE_TYPES_FILE_WITH_EXTERN_STRING) SED_AFTER_STRING=$(KEYSTORE_TYPES_FILE_WITHOUT_EXTERN_STRING)
+	$(MAKE) _sed_file SED_FILE_PATH=$(KEYSTORE_ADMIN_TYPES_FILE_PATH) SED_BEFORE_STRING=$(KEYSTORE_ADMIN_TYPES_FILE_WITH_EXTERN_STRING) SED_AFTER_STRING=$(KEYSTORE_ADMIN_TYPES_FILE_WITHOUT_EXTERN_STRING)
 
 _sed_index_file_remove_extern:
 	$(MAKE) _sed_file SED_FILE_PATH=$(MPL_CORE_INDEX_FILE_PATH) SED_BEFORE_STRING=$(MPL_CORE_INDEX_FILE_WITH_EXTERN_STRING) SED_AFTER_STRING=$(MPL_CORE_INDEX_FILE_WITHOUT_EXTERN_STRING)
 	$(MAKE) _sed_file SED_FILE_PATH=$(KEYSTORE_INDEX_FILE_PATH) SED_BEFORE_STRING=$(KEYSTORE_INDEX_FILE_WITH_EXTERN_STRING) SED_AFTER_STRING=$(KEYSTORE_INDEX_FILE_WITHOUT_EXTERN_STRING)
+	$(MAKE) _sed_file SED_FILE_PATH=$(KEYSTORE_ADMIN_INDEX_FILE_PATH) SED_BEFORE_STRING=$(KEYSTORE_ADMIN_INDEX_FILE_WITH_EXTERN_STRING) SED_AFTER_STRING=$(KEYSTORE_ADMIN_INDEX_FILE_WITHOUT_EXTERN_STRING)
 	$(MAKE) _sed_file SED_FILE_PATH=$(SYNCHRONIZED_LOCAL_CMC_FILE_PATH) SED_BEFORE_STRING=$(SYNCHRONIZED_LOCAL_CMC_WITH_EXTERN_STRING) SED_AFTER_STRING=$(SYNCHRONIZED_LOCAL_CMC_WITHOUT_EXTERN_STRING)
 	$(MAKE) _sed_file SED_FILE_PATH=$(STORM_TRACKING_CMC_FILE_PATH) SED_BEFORE_STRING=$(STORM_TRACKING_CMC_WITH_EXTERN_STRING) SED_AFTER_STRING=$(STORM_TRACKING_CMC_WITHOUT_EXTERN_STRING)
 
 _sed_types_file_add_extern:
 	$(MAKE) _sed_file SED_FILE_PATH=$(MPL_CORE_TYPES_FILE_PATH) SED_BEFORE_STRING=$(MPL_CORE_TYPES_FILE_WITHOUT_EXTERN_STRING) SED_AFTER_STRING=$(MPL_CORE_TYPES_FILE_WITH_EXTERN_STRING)
 	$(MAKE) _sed_file SED_FILE_PATH=$(KEYSTORE_TYPES_FILE_PATH) SED_BEFORE_STRING=$(KEYSTORE_TYPES_FILE_WITHOUT_EXTERN_STRING) SED_AFTER_STRING=$(KEYSTORE_TYPES_FILE_WITH_EXTERN_STRING)
+	$(MAKE) _sed_file SED_FILE_PATH=$(KEYSTORE_ADMIN_TYPES_FILE_PATH) SED_BEFORE_STRING=$(KEYSTORE_ADMIN_TYPES_FILE_WITHOUT_EXTERN_STRING) SED_AFTER_STRING=$(KEYSTORE_ADMIN_TYPES_FILE_WITH_EXTERN_STRING)
 
 _sed_index_file_add_extern:
 	$(MAKE) _sed_file SED_FILE_PATH=$(MPL_CORE_INDEX_FILE_PATH) SED_BEFORE_STRING=$(MPL_CORE_INDEX_FILE_WITHOUT_EXTERN_STRING) SED_AFTER_STRING=$(MPL_CORE_INDEX_FILE_WITH_EXTERN_STRING)
 	$(MAKE) _sed_file SED_FILE_PATH=$(KEYSTORE_INDEX_FILE_PATH) SED_BEFORE_STRING=$(KEYSTORE_INDEX_FILE_WITHOUT_EXTERN_STRING) SED_AFTER_STRING=$(KEYSTORE_INDEX_FILE_WITH_EXTERN_STRING)
+	$(MAKE) _sed_file SED_FILE_PATH=$(KEYSTORE_ADMIN_INDEX_FILE_PATH) SED_BEFORE_STRING=$(KEYSTORE_ADMIN_INDEX_FILE_WITHOUT_EXTERN_STRING) SED_AFTER_STRING=$(KEYSTORE_ADMIN_INDEX_FILE_WITH_EXTERN_STRING)
 	$(MAKE) _sed_file SED_FILE_PATH=$(SYNCHRONIZED_LOCAL_CMC_FILE_PATH) SED_BEFORE_STRING=$(SYNCHRONIZED_LOCAL_CMC_WITHOUT_EXTERN_STRING) SED_AFTER_STRING=$(SYNCHRONIZED_LOCAL_CMC_WITH_EXTERN_STRING)
 	$(MAKE) _sed_file SED_FILE_PATH=$(STORM_TRACKING_CMC_FILE_PATH) SED_BEFORE_STRING=$(STORM_TRACKING_CMC_WITHOUT_EXTERN_STRING) SED_AFTER_STRING=$(STORM_TRACKING_CMC_WITH_EXTERN_STRING)
 
@@ -146,3 +170,7 @@ PYTHON_DEPENDENCY_MODULE_NAMES := \
 	--dependency-library-name=com.amazonaws.dynamodb=aws_cryptography_internal_dynamodb \
 	--dependency-library-name=aws.cryptography.materialProviders=aws_cryptographic_material_providers \
 	--dependency-library-name=aws.cryptography.keyStore=aws_cryptographic_material_providers \
+	--dependency-library-name=aws.cryptography.keyStoreAdmin=aws_cryptographic_material_providers \
+
+test_example_java:
+	$(GRADLEW) -p runtimes/java cleanTestExamples testExamples

AwsCryptographicMaterialProviders/codegen-patches/AwsCryptographicMaterialProviders/dotnet/dafny-4.8.0.patch

@@ -0,0 +1,15 @@
+diff --git b/AwsCryptographicMaterialProviders/runtimes/net/Generated/AwsCryptographicMaterialProviders/TypeConversion.cs a/AwsCryptographicMaterialProviders/runtimes/net/Generated/AwsCryptographicMaterialProviders/TypeConversion.cs
+index 0b153802b..56aef9ec6 100644
+--- b/AwsCryptographicMaterialProviders/runtimes/net/Generated/AwsCryptographicMaterialProviders/TypeConversion.cs
++++ a/AwsCryptographicMaterialProviders/runtimes/net/Generated/AwsCryptographicMaterialProviders/TypeConversion.cs
+@@ -3903,7 +3903,9 @@ namespace AWS.Cryptography.MaterialProviders
+             dafnyVal._ComAmazonawsDynamodb
+           );
+         case software.amazon.cryptography.materialproviders.internaldafny.types.Error_ComAmazonawsKms dafnyVal:
+-          return Com.Amazonaws.KMS.TypeConversion.FromDafny_CommonError(
++          // BEGIN MANUAL EDIT
++          return Com.Amazonaws.Kms.TypeConversion.FromDafny_CommonError(
++            // END MANUAL EDIT
+             dafnyVal._ComAmazonawsKms
+           );
+         case software.amazon.cryptography.materialproviders.internaldafny.types.Error_AwsCryptographicMaterialProvidersException dafnyVal:

AwsCryptographicMaterialProviders/codegen-patches/AwsCryptographyKeyStore/dafny/dafny-4.8.0.patch

@@ -0,0 +1,13 @@
+diff --git b/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/Model/AwsCryptographyKeyStoreTypes.dfy a/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/Model/AwsCryptographyKeyStoreTypes.dfy
+index 5764797e..4310b660 100644
+--- b/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/Model/AwsCryptographyKeyStoreTypes.dfy
++++ a/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/Model/AwsCryptographyKeyStoreTypes.dfy
+@@ -794,7 +794,7 @@ abstract module AbstractAwsCryptographyKeyStoreService
+   import opened Types = AwsCryptographyKeyStoreTypes
+   import Operations : AbstractAwsCryptographyKeyStoreOperations
+   function method DefaultKeyStoreConfig(): KeyStoreConfig
+-  method KeyStore(config: KeyStoreConfig := DefaultKeyStoreConfig())
++  method {:vcs_split_on_every_assert} {:rlimit 90500000} KeyStore(config: KeyStoreConfig := DefaultKeyStoreConfig())
+     returns (res: Result<KeyStoreClient, Error>)
+     requires config.ddbClient.Some? ==>
+                config.ddbClient.value.ValidState()

AwsCryptographicMaterialProviders/codegen-patches/AwsCryptographyKeyStore/dafny/dafny-4.9.0.patch

@@ -0,0 +1,13 @@
+diff --git b/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/Model/AwsCryptographyKeyStoreTypes.dfy a/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/Model/AwsCryptographyKeyStoreTypes.dfy
+index 25bd45838..3ddedde75 100644
+--- b/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/Model/AwsCryptographyKeyStoreTypes.dfy
++++ a/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/Model/AwsCryptographyKeyStoreTypes.dfy
+@@ -611,7 +611,7 @@ abstract module AbstractAwsCryptographyKeyStoreService
+   import opened Types = AwsCryptographyKeyStoreTypes
+   import Operations : AbstractAwsCryptographyKeyStoreOperations
+   function method DefaultKeyStoreConfig(): KeyStoreConfig
+-  method KeyStore(config: KeyStoreConfig := DefaultKeyStoreConfig())
++  method {:isoluate_asserations} {:resource_limit 94000000 } KeyStore(config: KeyStoreConfig := DefaultKeyStoreConfig())
+     returns (res: Result<KeyStoreClient, Error>)
+     requires config.ddbClient.Some? ==>
+                config.ddbClient.value.ValidState()