[Draft] Python compatability with Java/NET

.github/actions/install_smithy_dafny_codegen_dependencies/action.yml

@@ -0,0 +1,21 @@
+#
+# This local action sets up code dependencies
+# to run Smithy-Dafny CI in GitHub Actions workflows.
+#
+
+name: "Install Smithy-Dafny codegen dependencies"
+description: "Install Java package dependencies required to run Smithy-Dafny codegen"
+runs:
+  using: "composite"
+  steps:
+    - name: Install smithy-dafny-codegen Rust dependencies locally
+      uses: gradle/gradle-build-action@v2
+      with:
+        arguments: :codegen-client:pTML :codegen-core:pTML :rust-runtime:pTML
+        build-root-directory: smithy-dafny/smithy-dafny-codegen-modules/smithy-rs
+
+    - name: Install smithy-dafny-codegen Python dependencies locally
+      uses: gradle/gradle-build-action@v2
+      with:
+        arguments: :smithy-python-codegen:pTML
+        build-root-directory: smithy-dafny/codegen/smithy-dafny-codegen-modules/smithy-python/codegen

.github/workflows/library_codegen.yml

@@ -42,7 +42,7 @@ jobs:
       # The specification submodule is private so we don't have access, but we don't need
       # it to verify the Dafny code. Instead we manually pull the submodules we DO need.
       - run: git submodule update --init libraries
-      - run: git submodule update --init smithy-dafny
+      - run: git submodule update --init --recursive smithy-dafny
 
       # Only used to format generated code
       # and to translate version strings such as "nightly-latest"
@@ -56,6 +56,15 @@ jobs:
         uses: actions/setup-dotnet@v3
         with:
           dotnet-version: ${{ matrix.dotnet-version }}
+
+      - name: Setup Java 17 for codegen
+        uses: actions/setup-java@v3
+        with:
+          distribution: "corretto"
+          java-version: "17"
+
+      - name: Install Smithy-Dafny codegen dependencies
+        uses: ./.github/actions/install_smithy_dafny_codegen_dependencies
 
       - uses: ./.github/actions/polymorph_codegen
         with:

.github/workflows/library_interop_tests.yml

@@ -25,7 +25,7 @@ jobs:
             ubuntu-latest,
             macos-12,
           ]
-        language: [java, net]
+        language: [java, net, python]
         # https://taskei.amazon.dev/tasks/CrypTool-5284
         dotnet-version: ["6.0.x"]
     runs-on: ${{ matrix.os }}
@@ -57,6 +57,16 @@ jobs:
           distribution: "corretto"
           java-version: 17
 
+      - name: Setup Python for running tests
+        uses: actions/setup-python@v4
+        with:
+          python-version: 3.11
+          architecture: x64
+      - run: |
+          python -m pip install --upgrade pip
+          pip install --upgrade tox
+          pip install poetry
+
       - name: Setup Dafny
         uses: dafny-lang/[email protected]
         with:
@@ -89,6 +99,8 @@ jobs:
           CORES=$(node -e 'console.log(os.cpus().length)')
           make transpile_net
 
+      # Python implementation is expected to be committed and doesn't need to be built
+
       - name: Setup gradle
         if: matrix.language == 'java'
         uses: gradle/gradle-build-action@v2
@@ -128,8 +140,8 @@ jobs:
             ubuntu-latest,
             macos-12,
           ]
-        encrypting_language: [java, net]
-        decrypting_language: [java, net]
+        encrypting_language: [java, net, python]
+        decrypting_language: [java, net, python]
         dotnet-version: ["6.0.x"]
     runs-on: ${{ matrix.os }}
     permissions:
@@ -166,6 +178,16 @@ jobs:
         with:
           distribution: "corretto"
           java-version: 17
+
+      - name: Setup Python for running tests
+        uses: actions/setup-python@v4
+        with:
+          python-version: 3.11
+          architecture: x64
+      - run: |
+          python -m pip install --upgrade pip
+          pip install --upgrade tox
+          pip install poetry
 
       - name: Setup Dafny
         uses: dafny-lang/[email protected]
@@ -199,6 +221,8 @@ jobs:
           CORES=$(node -e 'console.log(os.cpus().length)')
           make transpile_net
 
+      # Python implementation is expected to be committed and doesn't need to be built
+
       - name: Download Encrypt Manifest Artifact
         uses: actions/download-artifact@v4
         with:

.github/workflows/library_python_tests.yml

@@ -0,0 +1,83 @@
+# This workflow performs tests in Python.
+name: Library Python 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:
+  testPython:
+    strategy:
+      fail-fast: false
+      matrix:
+        library:
+          [
+            StandardLibrary,
+            AwsCryptographyPrimitives,
+            ComAmazonawsKms,
+            ComAmazonawsDynamodb,
+            AwsCryptographicMaterialProviders,
+            TestVectorsAwsCryptographicMaterialProviders,
+          ]
+        python-version: ["3.11"]
+        os: [
+            ubuntu-latest,
+            macos-latest,
+          ]
+    runs-on: ${{ matrix.os }}
+    defaults:
+      run:
+        shell: bash
+    permissions:
+      id-token: write
+      contents: read
+    steps:
+      - name: Support longpaths on Git checkout
+        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-MPL-Dafny-Role-us-west-2
+          role-session-name: PythonTests
+
+      - uses: actions/checkout@v4
+      # The specification submodule is private so we don't have access, but we don't need
+      # it to verify the Dafny code. Instead we manually pull the submodules we DO need.
+      - 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 Python ${{ matrix.python-version }} for running tests
+        uses: actions/setup-python@v4
+        with:
+          python-version: ${{ matrix.python-version }}
+          architecture: x64
+      - run: |
+          python -m pip install --upgrade pip
+          pip install --upgrade tox
+          pip install poetry
+
+      # We would build the Dafny implementation here,
+      # but Python libraries will commit their generated Dafny.
+
+      - name: Test ${{ matrix.library }}
+        working-directory: ./${{ matrix.library }}
+        shell: bash
+        run: |
+          make test_python

.github/workflows/pull.yml

@@ -34,6 +34,12 @@ jobs:
     uses: ./.github/workflows/library_net_tests.yml
     with:
       dafny: ${{needs.getVersion.outputs.version}}
+  pr-ci-python:
+    needs: getVersion
+    uses: ./.github/workflows/library_python_tests.yml
+    with:
+      # TODO: Once minimum Dafny version is 4.7.0, point this at `getVersion` output
+      dafny: 4.7.0
   pr-interop-test:
     needs: getVersion
     uses: ./.github/workflows/library_interop_tests.yml

.gitmodules

@@ -3,7 +3,7 @@
 	url = https://github.com/dafny-lang/libraries.git 
 [submodule "smithy-dafny"]
 	path = smithy-dafny
-	url = https://robin-aws@github.com/smithy-lang/smithy-dafny.git
+	url = https://github.com/smithy-lang/smithy-dafny.git
 [submodule "aws-encryption-sdk-specification"]
 	path = aws-encryption-sdk-specification
 	url = https://github.com/awslabs/aws-encryption-sdk-specification.git 

AwsCryptographicMaterialProviders/Makefile

@@ -3,6 +3,8 @@
 
 CORES=2
 
+ENABLE_EXTERN_PROCESSING=1
+
 include ../SharedMakefileV2.mk
 
 PROJECT_SERVICES := \
@@ -44,6 +46,52 @@ SERVICE_DEPS_AwsCryptographyKeyStore := \
 	ComAmazonawsDynamodb \
 	AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders \
 
+# 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"
+
+MPL_CORE_INDEX_FILE_PATH=dafny/AwsCryptographicMaterialProviders/src/Index.dfy
+MPL_CORE_INDEX_FILE_WITH_EXTERN_STRING="module {:extern \"software.amazon.cryptography.materialproviders.internaldafny\" } MaterialProviders refines AbstractAwsCryptographyMaterialProvidersService"
+MPL_CORE_INDEX_FILE_WITHOUT_EXTERN_STRING="module MaterialProviders refines AbstractAwsCryptographyMaterialProvidersService"
+
+KEYSTORE_TYPES_FILE_PATH=dafny/AwsCryptographyKeystore/Model/AwsCryptographyKeyStoreTypes.dfy
+KEYSTORE_TYPES_FILE_WITH_EXTERN_STRING="module {:extern \"software.amazon.cryptography.keystore.internaldafny.types\" } AwsCryptographyKeyStoreTypes"
+KEYSTORE_TYPES_FILE_WITHOUT_EXTERN_STRING="module AwsCryptographyKeyStoreTypes"
+
+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"
+
+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 {"
+
+STORM_TRACKING_CMC_FILE_PATH=dafny/AwsCryptographicMaterialProviders/src/CMCs/StormTrackingCMC.dfy
+STORM_TRACKING_CMC_WITH_EXTERN_STRING="module {:options \"\/functionSyntax:4\" } {:extern \"software.amazon.cryptography.internaldafny.StormTrackingCMC\" } StormTrackingCMC {"
+STORM_TRACKING_CMC_WITHOUT_EXTERN_STRING="module {:options \"\/functionSyntax:4\" } StormTrackingCMC {"
+
+_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)
+
+_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=$(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)
+
+_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=$(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)
+
 # Python
 
 PYTHON_MODULE_NAME=aws_cryptographic_materialproviders

AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/AwsCryptographyMaterialProvidersOperations.dfy

@@ -55,7 +55,7 @@ module AwsCryptographyMaterialProvidersOperations refines AbstractAwsCryptograph
   import StormTracker
   import StormTrackingCMC
   import Crypto = AwsCryptographyPrimitivesTypes
-  import Aws.Cryptography.Primitives
+  import AtomicPrimitives
   import opened AwsKmsUtils
   import DefaultClientSupplier
   import Materials
@@ -68,7 +68,7 @@ module AwsCryptographyMaterialProvidersOperations refines AbstractAwsCryptograph
   import RequiredEncryptionContextCMM
 
   datatype Config = Config(
-    nameonly crypto: Primitives.AtomicPrimitivesClient
+    nameonly crypto: AtomicPrimitives.AtomicPrimitivesClient
   )
 
   type InternalConfig = Config

AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/CMMs/DefaultCMM.dfy

@@ -19,15 +19,16 @@ module DefaultCMM {
   import UTF8
   import Types = AwsCryptographyMaterialProvidersTypes
   import Crypto = AwsCryptographyPrimitivesTypes
-  import Aws.Cryptography.Primitives
+  import AtomicPrimitives
   import Defaults
   import Commitment
   import Seq
+  import SortedSets
 
   class DefaultCMM
     extends CMM.VerifiableInterface
   {
-    const cryptoPrimitives: Primitives.AtomicPrimitivesClient
+    const cryptoPrimitives: AtomicPrimitives.AtomicPrimitivesClient
 
     predicate ValidState()
       ensures ValidState() ==> History in Modifies
@@ -50,7 +51,7 @@ module DefaultCMM {
       //# the caller MUST provide the following value:
       //# - [Keyring](#keyring)
       k: Types.IKeyring,
-      c: Primitives.AtomicPrimitivesClient
+      c: AtomicPrimitives.AtomicPrimitivesClient
     )
       requires k.ValidState() && c.ValidState()
       ensures keyring == k && cryptoPrimitives == c
@@ -329,7 +330,7 @@ module DefaultCMM {
     //# - The operations made on the encryption context on the Get Encryption Materials call
     //# SHOULD be inverted on the Decrypt Materials call.
 
-    method DecryptMaterials'(
+    method {:vcs_split_on_every_assert} DecryptMaterials'(
       input: Types.DecryptMaterialsInput
     )
       returns (output: Result<Types.DecryptMaterialsOutput, Types.Error>)
@@ -478,25 +479,36 @@ module DefaultCMM {
       var requiredEncryptionContextKeys := [];
       if input.reproducedEncryptionContext.Some? {
         var keysSet := input.reproducedEncryptionContext.value.Keys;
-        while keysSet != {}
+        ghost var keysSet' := keysSet;
+        var keysSeq := SortedSets.ComputeSetToSequence(keysSet);
+        var i := 0;
+        while i < |keysSeq|
+          invariant Seq.HasNoDuplicates(keysSeq)
+          invariant forall j | 0 <= j < i && i < |keysSeq| :: keysSeq[j] !in keysSet'
+          invariant forall j | i <= j < |keysSeq| :: keysSeq[j] in keysSet'
+          invariant |keysSet'| == |keysSeq| - i
           invariant forall key
                       |
                       && key in input.reproducedEncryptionContext.value
                       && key in input.encryptionContext
-                      && key !in keysSet
+                      && key !in keysSet'
                       :: input.reproducedEncryptionContext.value[key] == input.encryptionContext[key]
           invariant forall key <- requiredEncryptionContextKeys
                       :: key !in input.encryptionContext
         {
-          var key :| key in keysSet;
+          var key := keysSeq[i];
           if key in input.encryptionContext {
             :- Need(input.reproducedEncryptionContext.value[key] == input.encryptionContext[key],
                     Types.AwsCryptographicMaterialProvidersException(
                       message := "Encryption context does not match reproduced encryption context."));
           } else {
             requiredEncryptionContextKeys :=  requiredEncryptionContextKeys + [key];
           }
-          keysSet := keysSet - {key};
+          keysSet' := keysSet' - {key};
+          i := i + 1;
+          assert forall j | i <= j < |keysSeq| :: keysSeq[j] in keysSet' by {
+            reveal Seq.HasNoDuplicates();
+          }
         }
       }