feat(Go): support DB-ESDK in Go

.github/workflows/ci_test_go.yml

@@ -0,0 +1,141 @@
+# This workflow performs tests in Go.
+name: Library Go 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
+      mpl-version:
+        description: "MPL version to use"
+        required: false
+        type: string
+      mpl-head:
+        description: "Running on MPL HEAD"
+        required: false
+        default: false
+        type: boolean
+
+jobs:
+  testGo:
+    strategy:
+      matrix:
+        library: [DynamoDbEncryption, TestVectors]
+        os: [ubuntu-22.04, macos-13]
+        go-version: ["1.23"]
+    runs-on: ${{ matrix.os }}
+    permissions:
+      id-token: write
+      contents: read
+    steps:
+      - name: Setup Docker
+        if: matrix.os == 'macos-13' && matrix.library == 'TestVectors'
+        uses: douglascamata/setup-docker-macos-action@v1-alpha
+
+      - name: Setup DynamoDB Local
+        if: matrix.library == 'TestVectors'
+        uses: rrainn/[email protected]
+        with:
+          port: 8000
+          cors: "*"
+
+      - name: Support longpaths
+        run: |
+          git config --global core.longpaths true
+
+      - name: Configure AWS Credentials
+        uses: aws-actions/configure-aws-credentials@v4
+        with:
+          aws-region: us-west-2
+          role-to-assume: arn:aws:iam::370957321024:role/GitHub-CI-DDBEC-Dafny-Role-us-west-2
+          role-session-name: DDBEC-Dafny-Java-Tests
+
+      - uses: actions/checkout@v3
+        with:
+          submodules: recursive
+
+      - name: Setup Dafny
+        uses: dafny-lang/[email protected]
+        with:
+          dafny-version: ${{ inputs.dafny }}
+
+      - name: Create temporary global.json
+        run: echo '{"sdk":{"rollForward":"latestFeature","version":"6.0.0"}}' > ./global.json
+
+      - name: Setup Java 17 for codegen
+        uses: actions/setup-java@v3
+        with:
+          distribution: "corretto"
+          java-version: "17"
+
+      - name: Update MPL submodule if using MPL HEAD
+        if: ${{ inputs.mpl-head == true }}
+        working-directory: submodules/MaterialProviders
+        run: |
+          git checkout main
+          git pull
+          git submodule update --init --recursive
+          git rev-parse HEAD
+
+      - name: Update project.properties if using MPL HEAD
+        if: ${{ inputs.mpl-head == true }}
+        run: |
+          sed "s/mplDependencyJavaVersion=.*/mplDependencyJavaVersion=${{inputs.mpl-version}}/g" project.properties > project.properties2; mv project.properties2 project.properties
+
+      - name: Install Go
+        uses: actions/setup-go@v5
+        with:
+          go-version: ${{ matrix.go-version }}
+
+      - name: Install Go imports
+        run: |
+          go install golang.org/x/tools/cmd/goimports@latest
+
+      - uses: actions/checkout@v3
+      - name: Init Submodules
+        shell: bash
+        run: |
+          git submodule update --init --recursive submodules/smithy-dafny
+          git submodule update --init --recursive submodules/MaterialProviders
+
+      - name: Install Smithy-Dafny codegen dependencies
+        uses: ./.github/actions/install_smithy_dafny_codegen_dependencies
+
+      - name: Build ${{ matrix.library }} implementation
+        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 transpile_go CORES=$CORES
+
+      - name: Regenerate code using smithy-dafny
+        shell: bash
+        working-directory: ./${{ matrix.library }}
+        run: |
+          make polymorph_go
+
+      - name: Copy ${{ matrix.library }} Vector Files
+        if: ${{ matrix.library == 'TestVectors' }}
+        shell: bash
+        working-directory: ./${{ matrix.library }}
+        run: |
+          cp runtimes/java/*.json runtimes/go/TestsFromDafny-go/
+
+      - name: Test ${{ matrix.library }}
+        working-directory: ./${{ matrix.library }}
+        run: |
+          make test_go
+
+      - name: Test Examples
+        if: matrix.library == 'DynamoDbEncryption'
+        working-directory: ./Examples/runtimes/go
+        run: |
+          go run main.go

.github/workflows/ci_todos.yml

@@ -17,8 +17,8 @@ jobs:
         shell: bash
         # TODOs may be committed as long as the same line contains a link to a Github Issue or refers to a CrypTool SIM.
         run: |
-          ALL_TODO_COUNT=$( { grep -r "TODO" . --exclude-dir=./releases --exclude-dir=./TestVectors/runtimes --exclude-dir=./submodules --exclude-dir=./.git --exclude=./.github/workflows/ci_todos.yml || true; } | wc -l)
-          GOOD_TODO_COUNT=$( { grep -r "TODO.*\(github.com\/.*issues.*\/[1-9][0-9]*\|CrypTool-[1-9][0-9]*\)" . --exclude-dir=./releases --exclude-dir=./submodules --exclude-dir=./.git  --exclude-dir=./TestVectors/runtimes --exclude=./.github/workflows/ci_todos.yml || true; } | wc -l)
+          ALL_TODO_COUNT=$( { grep -r "TODO" . --exclude-dir=./releases --exclude-dir=./TestVectors/runtimes --exclude-dir=./submodules --exclude-dir=./.git --exclude=./.github/workflows/ci_todos.yml | grep -v "context\.TODO()" || true; } | wc -l)
+          GOOD_TODO_COUNT=$( { grep -r "TODO.*\(github.com\/.*issues.*\/[1-9][0-9]*\|CrypTool-[1-9][0-9]*\)" . --exclude-dir=./releases --exclude-dir=./submodules --exclude-dir=./.git  --exclude-dir=./TestVectors/runtimes --exclude=./.github/workflows/ci_todos.yml | grep -v "context\.TODO()" || true; } | wc -l)
           if [ "$ALL_TODO_COUNT" != "$GOOD_TODO_COUNT" ]; then
             exit 1;
           fi

.github/workflows/pull.yml

@@ -54,6 +54,11 @@ jobs:
     uses: ./.github/workflows/library_rust_tests.yml
     with:
       dafny: ${{needs.getVersion.outputs.version}}
+  pr-ci-go:
+    needs: getVersion
+    uses: ./.github/workflows/ci_test_go.yml
+    with:
+      dafny: ${{needs.getVersion.outputs.version}}
   pr-ci-net-test-vectors:
     needs: getVersion
     uses: ./.github/workflows/ci_test_vector_net.yml
@@ -78,6 +83,7 @@ jobs:
       - pr-ci-java-examples
       - pr-ci-net
       - pr-ci-rust
+      - pr-ci-go
       - pr-ci-net-test-vectors
       - pr-ci-net-examples
     runs-on: ubuntu-22.04

.github/workflows/push.yml

@@ -56,6 +56,11 @@ jobs:
     uses: ./.github/workflows/library_rust_tests.yml
     with:
       dafny: ${{needs.getVersion.outputs.version}}
+  pr-ci-go:
+    needs: getVersion
+    uses: ./.github/workflows/ci_test_go.yml
+    with:
+      dafny: ${{needs.getVersion.outputs.version}}
   pr-ci-net-test-vectors:
     needs: getVersion
     uses: ./.github/workflows/ci_test_vector_net.yml

DynamoDbEncryption/Makefile

@@ -4,6 +4,7 @@
 CORES=2
 
 TRANSPILE_TESTS_IN_RUST=1
+ENABLE_EXTERN_PROCESSING=1
 
 include ../SharedMakefile.mk
 
@@ -99,3 +100,92 @@ SERVICE_DEPS_DynamoDbEncryptionTransforms := \
 	DynamoDbEncryption/dafny/DynamoDbEncryption \
 	DynamoDbEncryption/dafny/StructuredEncryption \
 	DynamoDbEncryption/dafny/DynamoDbItemEncryptor
+
+# Go
+# TODO-Go-ORR: Define the name later https://sim.amazon.com/issues/CrypTool-5444
+# This will probably get changes to */releases/go/* but I will bring this to the team later.
+GO_MODULE_NAME="github.com/aws/aws-database-encryption-sdk-dynamodb"
+
+GO_DEPENDENCY_MODULE_NAMES := \
+	--dependency-library-name=aws.cryptography.primitives=github.com/aws/aws-cryptographic-material-providers-library/releases/go/primitives \
+	--dependency-library-name=com.amazonaws.kms=github.com/aws/aws-cryptographic-material-providers-library/releases/go/kms \
+	--dependency-library-name=com.amazonaws.dynamodb=github.com/aws/aws-cryptographic-material-providers-library/releases/go/dynamodb \
+	--dependency-library-name=aws.cryptography.materialProviders=github.com/aws/aws-cryptographic-material-providers-library/releases/go/mpl \
+	--dependency-library-name=aws.cryptography.keyStore=github.com/aws/aws-cryptographic-material-providers-library/releases/go/mpl \
+	--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 \
+	--dependency-library-name=aws.cryptography.dbEncryptionSdk.structuredEncryption=github.com/aws/aws-database-encryption-sdk-dynamodb \
+	--dependency-library-name=aws.cryptography.dbEncryptionSdk.dynamoDb=github.com/aws/aws-database-encryption-sdk-dynamodb \
+	--dependency-library-name=aws.cryptography.dbEncryptionSdk.dynamoDb.itemEncryptor=github.com/aws/aws-database-encryption-sdk-dynamodb \
+	--dependency-library-name=aws.cryptography.dbEncryptionSdk.dynamoDb.transforms=github.com/aws/aws-database-encryption-sdk-dynamodb
+
+TRANSLATION_RECORD_GO := \
+    submodules/MaterialProviders/StandardLibrary/runtimes/go/ImplementationFromDafny-go/ImplementationFromDafny-go.dtr \
+    submodules/MaterialProviders/ComAmazonawsKms/runtimes/go/ImplementationFromDafny-go/ImplementationFromDafny-go.dtr \
+    submodules/MaterialProviders/ComAmazonawsDynamodb/runtimes/go/ImplementationFromDafny-go/ImplementationFromDafny-go.dtr \
+    submodules/MaterialProviders/AwsCryptographyPrimitives/runtimes/go/ImplementationFromDafny-go/ImplementationFromDafny-go.dtr \
+	submodules/MaterialProviders/AwsCryptographicMaterialProviders/runtimes/go/ImplementationFromDafny-go/ImplementationFromDafny-go.dtr
+
+# Constants for languages that drop extern names (Python, Go)
+
+DYNAMODB_TYPES_FILE_PATH=dafny/DynamoDbEncryption/Model/AwsCryptographyDbEncryptionSdkDynamoDbTypes.dfy
+DYNAMODB_TYPES_FILE_WITH_EXTERN_STRING="module {:extern \"software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types\" } AwsCryptographyDbEncryptionSdkDynamoDbTypes"
+DYNAMODB_TYPES_FILE_WITHOUT_EXTERN_STRING="module AwsCryptographyDbEncryptionSdkDynamoDbTypes"
+
+DYNAMODB_INDEX_FILE_PATH=dafny/DynamoDbEncryption/src/Index.dfy
+DYNAMODB_INDEX_FILE_WITH_EXTERN_STRING="module {:extern \"software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny\" } DynamoDbEncryption"
+DYNAMODB_INDEX_FILE_WITHOUT_EXTERN_STRING="module DynamoDbEncryption"
+
+ITEMENCRYPTOR_TYPES_FILE_PATH=dafny/DynamoDbItemEncryptor/Model/AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorTypes.dfy
+ITEMENCRYPTOR_TYPES_FILE_WITH_EXTERN_STRING="module {:extern \"software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.internaldafny.types\" } AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorTypes"
+ITEMENCRYPTOR_TYPES_FILE_WITHOUT_EXTERN_STRING="module AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorTypes"
+
+ITEMENCRYPTOR_INDEX_FILE_PATH=dafny/DynamoDbItemEncryptor/src/Index.dfy
+ITEMENCRYPTOR_INDEX_FILE_WITH_EXTERN_STRING="module {:extern \"software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.internaldafny\" } DynamoDbItemEncryptor"
+ITEMENCRYPTOR_INDEX_FILE_WITHOUT_EXTERN_STRING="module DynamoDbItemEncryptor"
+
+ITEMENCRYPTOR_LEGACY_FILE_PATH=dafny/DynamoDbItemEncryptor/src/InternalLegacyOverride.dfy
+ITEMENCRYPTOR_LEGACY_FILE_WITH_EXTERN_STRING="module {:extern \"software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.internaldafny.legacy\"} InternalLegacyOverride {"
+ITEMENCRYPTOR_LEGACY_FILE_WITHOUT_EXTERN_STRING="module InternalLegacyOverride {"
+
+TRANSFORMS_TYPES_FILE_PATH=dafny/DynamoDbEncryptionTransforms/Model/AwsCryptographyDbEncryptionSdkDynamoDbTransformsTypes.dfy
+TRANSFORMS_TYPES_FILE_WITH_EXTERN_STRING="module {:extern \"software.amazon.cryptography.dbencryptionsdk.dynamodb.transforms.internaldafny.types\" } AwsCryptographyDbEncryptionSdkDynamoDbTransformsTypes"
+TRANSFORMS_TYPES_FILE_WITHOUT_EXTERN_STRING="module AwsCryptographyDbEncryptionSdkDynamoDbTransformsTypes"
+
+TRANSFORMS_INDEX_FILE_PATH=dafny/DynamoDbEncryptionTransforms/src/Index.dfy
+TRANSFORMS_INDEX_FILE_WITH_EXTERN_STRING="module {:extern \"software.amazon.cryptography.dbencryptionsdk.dynamodb.transforms.internaldafny\" } DynamoDbEncryptionTransforms"
+TRANSFORMS_INDEX_FILE_WITHOUT_EXTERN_STRING="module DynamoDbEncryptionTransforms"
+
+STRUCTUREDENCRYPTION_TYPES_FILE_PATH=dafny/StructuredEncryption/Model/AwsCryptographyDbEncryptionSdkStructuredEncryptionTypes.dfy
+STRUCTUREDENCRYPTION_TYPES_FILE_WITH_EXTERN_STRING="module {:extern \"software.amazon.cryptography.dbencryptionsdk.structuredencryption.internaldafny.types\" } AwsCryptographyDbEncryptionSdkStructuredEncryptionTypes"
+STRUCTUREDENCRYPTION_TYPES_FILE_WITHOUT_EXTERN_STRING="module AwsCryptographyDbEncryptionSdkStructuredEncryptionTypes"
+
+STRUCTUREDENCRYPTION_INDEX_FILE_PATH=dafny/StructuredEncryption/src/Index.dfy
+STRUCTUREDENCRYPTION_INDEX_FILE_WITH_EXTERN_STRING="module {:extern \"software.amazon.cryptography.dbencryptionsdk.structuredencryption.internaldafny\" } StructuredEncryption"
+STRUCTUREDENCRYPTION_INDEX_FILE_WITHOUT_EXTERN_STRING="module StructuredEncryption"
+
+_sed_types_file_remove_extern:
+	$(MAKE) _sed_file SED_FILE_PATH=$(DYNAMODB_TYPES_FILE_PATH) SED_BEFORE_STRING=$(DYNAMODB_TYPES_FILE_WITH_EXTERN_STRING) SED_AFTER_STRING=$(DYNAMODB_TYPES_FILE_WITHOUT_EXTERN_STRING)
+	$(MAKE) _sed_file SED_FILE_PATH=$(ITEMENCRYPTOR_TYPES_FILE_PATH) SED_BEFORE_STRING=$(ITEMENCRYPTOR_TYPES_FILE_WITH_EXTERN_STRING) SED_AFTER_STRING=$(ITEMENCRYPTOR_TYPES_FILE_WITHOUT_EXTERN_STRING)
+	$(MAKE) _sed_file SED_FILE_PATH=$(TRANSFORMS_TYPES_FILE_PATH) SED_BEFORE_STRING=$(TRANSFORMS_TYPES_FILE_WITH_EXTERN_STRING) SED_AFTER_STRING=$(TRANSFORMS_TYPES_FILE_WITHOUT_EXTERN_STRING)
+	$(MAKE) _sed_file SED_FILE_PATH=$(STRUCTUREDENCRYPTION_TYPES_FILE_PATH) SED_BEFORE_STRING=$(STRUCTUREDENCRYPTION_TYPES_FILE_WITH_EXTERN_STRING) SED_AFTER_STRING=$(STRUCTUREDENCRYPTION_TYPES_FILE_WITHOUT_EXTERN_STRING)
+
+_sed_index_file_remove_extern:
+	$(MAKE) _sed_file SED_FILE_PATH=$(DYNAMODB_INDEX_FILE_PATH) SED_BEFORE_STRING=$(DYNAMODB_INDEX_FILE_WITH_EXTERN_STRING) SED_AFTER_STRING=$(DYNAMODB_INDEX_FILE_WITHOUT_EXTERN_STRING)
+	$(MAKE) _sed_file SED_FILE_PATH=$(ITEMENCRYPTOR_INDEX_FILE_PATH) SED_BEFORE_STRING=$(ITEMENCRYPTOR_INDEX_FILE_WITH_EXTERN_STRING) SED_AFTER_STRING=$(ITEMENCRYPTOR_INDEX_FILE_WITHOUT_EXTERN_STRING)
+	$(MAKE) _sed_file SED_FILE_PATH=$(ITEMENCRYPTOR_LEGACY_FILE_PATH) SED_BEFORE_STRING=$(ITEMENCRYPTOR_LEGACY_FILE_WITH_EXTERN_STRING) SED_AFTER_STRING=$(ITEMENCRYPTOR_LEGACY_FILE_WITHOUT_EXTERN_STRING)
+	$(MAKE) _sed_file SED_FILE_PATH=$(TRANSFORMS_INDEX_FILE_PATH) SED_BEFORE_STRING=$(TRANSFORMS_INDEX_FILE_WITH_EXTERN_STRING) SED_AFTER_STRING=$(TRANSFORMS_INDEX_FILE_WITHOUT_EXTERN_STRING)
+	$(MAKE) _sed_file SED_FILE_PATH=$(STRUCTUREDENCRYPTION_INDEX_FILE_PATH) SED_BEFORE_STRING=$(STRUCTUREDENCRYPTION_INDEX_FILE_WITH_EXTERN_STRING) SED_AFTER_STRING=$(STRUCTUREDENCRYPTION_INDEX_FILE_WITHOUT_EXTERN_STRING)
+
+_sed_types_file_add_extern:
+	$(MAKE) _sed_file SED_FILE_PATH=$(DYNAMODB_TYPES_FILE_PATH) SED_BEFORE_STRING=$(DYNAMODB_TYPES_FILE_WITHOUT_EXTERN_STRING) SED_AFTER_STRING=$(DYNAMODB_TYPES_FILE_WITH_EXTERN_STRING)
+	$(MAKE) _sed_file SED_FILE_PATH=$(ITEMENCRYPTOR_TYPES_FILE_PATH) SED_BEFORE_STRING=$(ITEMENCRYPTOR_TYPES_FILE_WITHOUT_EXTERN_STRING) SED_AFTER_STRING=$(ITEMENCRYPTOR_TYPES_FILE_WITH_EXTERN_STRING)
+	$(MAKE) _sed_file SED_FILE_PATH=$(TRANSFORMS_TYPES_FILE_PATH) SED_BEFORE_STRING=$(TRANSFORMS_TYPES_FILE_WITHOUT_EXTERN_STRING) SED_AFTER_STRING=$(TRANSFORMS_TYPES_FILE_WITH_EXTERN_STRING)
+	$(MAKE) _sed_file SED_FILE_PATH=$(STRUCTUREDENCRYPTION_TYPES_FILE_PATH) SED_BEFORE_STRING=$(STRUCTUREDENCRYPTION_TYPES_FILE_WITHOUT_EXTERN_STRING) SED_AFTER_STRING=$(STRUCTUREDENCRYPTION_TYPES_FILE_WITH_EXTERN_STRING)
+
+_sed_index_file_add_extern:
+	$(MAKE) _sed_file SED_FILE_PATH=$(DYNAMODB_INDEX_FILE_PATH) SED_BEFORE_STRING=$(DYNAMODB_INDEX_FILE_WITHOUT_EXTERN_STRING) SED_AFTER_STRING=$(DYNAMODB_INDEX_FILE_WITH_EXTERN_STRING)
+	$(MAKE) _sed_file SED_FILE_PATH=$(ITEMENCRYPTOR_INDEX_FILE_PATH) SED_BEFORE_STRING=$(ITEMENCRYPTOR_INDEX_FILE_WITHOUT_EXTERN_STRING) SED_AFTER_STRING=$(ITEMENCRYPTOR_INDEX_FILE_WITH_EXTERN_STRING)
+	$(MAKE) _sed_file SED_FILE_PATH=$(ITEMENCRYPTOR_LEGACY_FILE_PATH) SED_BEFORE_STRING=$(ITEMENCRYPTOR_LEGACY_FILE_WITHOUT_EXTERN_STRING) SED_AFTER_STRING=$(ITEMENCRYPTOR_LEGACY_FILE_WITH_EXTERN_STRING)
+	$(MAKE) _sed_file SED_FILE_PATH=$(TRANSFORMS_INDEX_FILE_PATH) SED_BEFORE_STRING=$(TRANSFORMS_INDEX_FILE_WITHOUT_EXTERN_STRING) SED_AFTER_STRING=$(TRANSFORMS_INDEX_FILE_WITH_EXTERN_STRING)
+	$(MAKE) _sed_file SED_FILE_PATH=$(STRUCTUREDENCRYPTION_INDEX_FILE_PATH) SED_BEFORE_STRING=$(STRUCTUREDENCRYPTION_INDEX_FILE_WITHOUT_EXTERN_STRING) SED_AFTER_STRING=$(STRUCTUREDENCRYPTION_INDEX_FILE_WITH_EXTERN_STRING)

DynamoDbEncryption/dafny/DynamoDbEncryption/src/Index.dfy

@@ -16,9 +16,8 @@ include "UpdateExpr.dfy"
 include "Util.dfy"
 include "Virtual.dfy"
 
-module
-  {:extern "software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny" }
-  DynamoDbEncryption refines AbstractAwsCryptographyDbEncryptionSdkDynamoDbService
+module {:extern "software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny" } DynamoDbEncryption
+  refines AbstractAwsCryptographyDbEncryptionSdkDynamoDbService
 {
   import Operations = AwsCryptographyDbEncryptionSdkDynamoDbOperations
 

DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/Index.dfy

@@ -5,9 +5,8 @@ include "DdbMiddlewareConfig.dfy"
 include "AwsCryptographyDbEncryptionSdkDynamoDbTransformsOperations.dfy"
 include "../../DynamoDbEncryption/src/ConfigToInfo.dfy"
 
-module
-  {:extern "software.amazon.cryptography.dbencryptionsdk.dynamodb.transforms.internaldafny" }
-  DynamoDbEncryptionTransforms refines AbstractAwsCryptographyDbEncryptionSdkDynamoDbTransformsService
+module {:extern "software.amazon.cryptography.dbencryptionsdk.dynamodb.transforms.internaldafny" } DynamoDbEncryptionTransforms
+  refines AbstractAwsCryptographyDbEncryptionSdkDynamoDbTransformsService
 {
   import opened DdbMiddlewareConfig
   import opened StandardLibrary

DynamoDbEncryption/dafny/DynamoDbItemEncryptor/src/Index.dfy

@@ -4,9 +4,8 @@
 include "AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations.dfy"
 include "Util.dfy"
 
-module
-  {:extern "software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.internaldafny" }
-  DynamoDbItemEncryptor refines AbstractAwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorService
+module {:extern "software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.internaldafny" } DynamoDbItemEncryptor
+  refines AbstractAwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorService
 {
   import opened DynamoDbItemEncryptorUtil
   import StructuredEncryption

DynamoDbEncryption/dafny/StructuredEncryption/src/Index.dfy

@@ -3,9 +3,8 @@
 
 include "AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations.dfy"
 
-module
-  {:extern "software.amazon.cryptography.dbencryptionsdk.structuredencryption.internaldafny" }
-  StructuredEncryption refines AbstractAwsCryptographyDbEncryptionSdkStructuredEncryptionService
+module {:extern "software.amazon.cryptography.dbencryptionsdk.structuredencryption.internaldafny" } StructuredEncryption
+  refines AbstractAwsCryptographyDbEncryptionSdkStructuredEncryptionService
 {
 
   import Operations = AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations