diff --git a/.github/workflows/library_interop_test_vectors.yml b/.github/workflows/library_interop_test_vectors.yml index 338bce5dc..60ee7a00a 100644 --- a/.github/workflows/library_interop_test_vectors.yml +++ b/.github/workflows/library_interop_test_vectors.yml @@ -25,14 +25,13 @@ jobs: ubuntu-22.04, macos-13, ] - language: [java, net, rust, go] + language: [java, net, rust, go, python] # https://taskei.amazon.dev/tasks/CrypTool-5284 dotnet-version: ["6.0.x"] runs-on: ${{ matrix.os }} permissions: id-token: write contents: read - steps: - name: Support longpaths on Git checkout run: | @@ -67,6 +66,17 @@ jobs: distribution: "corretto" java-version: 17 + - name: Setup Python for running tests + if: matrix.language == 'python' + 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 Rust Toolchain for GitHub CI if: matrix.language == 'rust' uses: actions-rust-lang/setup-rust-toolchain@v1.10.1 @@ -144,6 +154,15 @@ jobs: CORES=$(node -e 'console.log(os.cpus().length)') make transpile_rust CORES=$CORES + - name: Build ${{ matrix.library }} implementation in Python + if: matrix.language == 'python' + 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_python CORES=$CORES + - name: Build ${{ matrix.library }} implementation in Go if: matrix.language == 'go' shell: bash @@ -187,6 +206,7 @@ jobs: testInteroperablity: needs: generateEncryptVectors strategy: + fail-fast: false matrix: library: [TestVectors] os: [ @@ -195,8 +215,8 @@ jobs: ubuntu-22.04, macos-13, ] - encrypting_language: [java, net, rust, go] - decrypting_language: [java, net, rust, go] + encrypting_language: [java, net, rust, go, python] + decrypting_language: [java, net, rust, go, python] # https://taskei.amazon.dev/tasks/CrypTool-5284 dotnet-version: ["6.0.x"] runs-on: ${{ matrix.os }} @@ -238,6 +258,17 @@ jobs: distribution: "corretto" java-version: 17 + - name: Setup Python for running tests + if: matrix.decrypting_language == 'python' + 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 Rust Toolchain for GitHub CI if: matrix.decrypting_language == 'rust' uses: actions-rust-lang/setup-rust-toolchain@v1.10.1 @@ -332,6 +363,14 @@ jobs: run: | make purge_polymorph_code + - name: Build ${{ matrix.library }} implementation in Python + if: matrix.decrypting_language == 'python' + shell: bash + working-directory: ./${{ matrix.library }} + run: | + CORES=$(node -e 'console.log(os.cpus().length)') + make transpile_python CORES=$CORES + - name: Download Encrypt Manifest Artifact uses: actions/download-artifact@v4 with: diff --git a/AwsEncryptionSDK/Makefile b/AwsEncryptionSDK/Makefile index 0fea756cc..129a13001 100644 --- a/AwsEncryptionSDK/Makefile +++ b/AwsEncryptionSDK/Makefile @@ -107,3 +107,20 @@ restore_directories: echo "Directory $$dir not found"; \ fi \ done + +PYTHON_MODULE_NAME=aws_encryption_sdk_dafny + +TRANSLATION_RECORD_PYTHON := \ + --translation-record ../mpl/StandardLibrary/runtimes/python/src/smithy_dafny_standard_library/internaldafny/generated/dafny_src-py.dtr \ + --translation-record ../mpl/ComAmazonawsKms/runtimes/python/src/aws_cryptography_internal_kms/internaldafny/generated/dafny_src-py.dtr \ + --translation-record ../mpl/ComAmazonawsDynamodb/runtimes/python/src/aws_cryptography_internal_dynamodb/internaldafny/generated/dafny_src-py.dtr \ + --translation-record ../mpl/AwsCryptographyPrimitives/runtimes/python/src/aws_cryptography_primitives/internaldafny/generated/dafny_src-py.dtr \ + --translation-record ../mpl/AwsCryptographicMaterialProviders/runtimes/python/src/aws_cryptographic_material_providers/internaldafny/generated/dafny_src-py.dtr + +PYTHON_DEPENDENCY_MODULE_NAMES := \ + --dependency-library-name=aws.cryptography.primitives=aws_cryptography_primitives \ + --dependency-library-name=com.amazonaws.kms=aws_cryptography_internal_kms \ + --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=smithy.api=aws_cryptographic_material_providers diff --git a/AwsEncryptionSDK/runtimes/java/README.md b/AwsEncryptionSDK/runtimes/java/README.md new file mode 100644 index 000000000..07ec46496 --- /dev/null +++ b/AwsEncryptionSDK/runtimes/java/README.md @@ -0,0 +1,10 @@ +# Important: Do not use this code. This package is AWS-internal. + +This is NOT the released version of the AWS Encryption SDK for Java. + +You can access the AWS Encryption SDK for Java at: + +- Github: https://github.com/aws/aws-encryption-sdk-java +- Maven: https://mvnrepository.com/artifact/com.amazonaws/aws-encryption-sdk-java + +This is an in-development rewrite of the AWS Encryption SDK for Java and should not be used until development is complete. diff --git a/AwsEncryptionSDK/runtimes/python/.gitignore b/AwsEncryptionSDK/runtimes/python/.gitignore new file mode 100644 index 000000000..9cb72dcab --- /dev/null +++ b/AwsEncryptionSDK/runtimes/python/.gitignore @@ -0,0 +1,16 @@ +# Python build artifacts +__pycache__ +**/__pycache__ +*.pyc +src/**.egg-info/ +build +poetry.lock +**/poetry.lock +dist + +# Dafny-generated Python +**/internaldafny/generated/*.py + +# Python test artifacts +.tox +.pytest_cache diff --git a/AwsEncryptionSDK/runtimes/python/README.md b/AwsEncryptionSDK/runtimes/python/README.md new file mode 100644 index 000000000..004925c3d --- /dev/null +++ b/AwsEncryptionSDK/runtimes/python/README.md @@ -0,0 +1,10 @@ +# Important: Do not use this code. This package is AWS-internal. + +This is NOT the released version of the AWS Encryption SDK for Python. + +You can access the AWS Encryption SDK for Python at: + +- Github: https://github.com/aws/aws-encryption-sdk-python +- PyPI: https://pypi.org/project/aws-encryption-sdk/ + +This is an in-development rewrite of the AWS Encryption SDK for Python and should not be used until development is complete. diff --git a/AwsEncryptionSDK/runtimes/python/pyproject.toml b/AwsEncryptionSDK/runtimes/python/pyproject.toml new file mode 100644 index 000000000..857cc9480 --- /dev/null +++ b/AwsEncryptionSDK/runtimes/python/pyproject.toml @@ -0,0 +1,36 @@ +[tool.poetry] +# Note: We should not release this library with this name. +# We should release this library under the name `aws-encryption-sdk`. +# But this repo's TestVectors test the released, native version of the ESDK, +# which has this name. +# The names conflict, and issues arise from this. +# When we are ready to release the Dafny-Python ESDK, we should rename this, +# but figure out if/how we can still test the native ESDK in this repo. +name = "aws-encryption-sdk-dafny" +version = "0.1.0" +description = "" +authors = ["AWS Crypto Tools "] +# Note: We should not release this library with this package name. +# We should release this library with the package name `aws_encryption_sdk`. +# But this repo's TestVectors test the released, native version of the ESDK, +# which has this name. +# The names conflict, and issues arise from this. +# When we are ready to release the Dafny-Python ESDK, we should rename this, +# but figure out if/how we can still test the native ESDK in this repo. +packages = [ + { include = "aws_encryption_sdk_dafny", from = "src" } +] +# Include generated internaldafny files in package distributions, +# even though they are not included in version control +include = ["**/internaldafny/generated/*.py"] + +[tool.poetry.dependencies] +python = "^3.11.0" +aws-cryptographic-material-providers = { path = "../../../mpl/AwsCryptographicMaterialProviders/runtimes/python", develop = false} + +[tool.poetry.group.test.dependencies] +pytest = "^7.4.0" + +[build-system] +requires = ["poetry-core<2.0.0"] +build-backend = "poetry.core.masonry.api" diff --git a/AwsEncryptionSDK/runtimes/python/src/aws_encryption_sdk_dafny/__init__.py b/AwsEncryptionSDK/runtimes/python/src/aws_encryption_sdk_dafny/__init__.py new file mode 100644 index 000000000..67a3d57bd --- /dev/null +++ b/AwsEncryptionSDK/runtimes/python/src/aws_encryption_sdk_dafny/__init__.py @@ -0,0 +1,5 @@ +# Copyright Amazon.com Inc. or its affiliates. All Rights Reserved. +# SPDX-License-Identifier: Apache-2.0 + +# Initialize generated Dafny +from .internaldafny.generated import module_ diff --git a/AwsEncryptionSDK/runtimes/python/src/aws_encryption_sdk_dafny/internaldafny/__init__.py b/AwsEncryptionSDK/runtimes/python/src/aws_encryption_sdk_dafny/internaldafny/__init__.py new file mode 100644 index 000000000..f94fd12a2 --- /dev/null +++ b/AwsEncryptionSDK/runtimes/python/src/aws_encryption_sdk_dafny/internaldafny/__init__.py @@ -0,0 +1,2 @@ +# Copyright Amazon.com Inc. or its affiliates. All Rights Reserved. +# SPDX-License-Identifier: Apache-2.0 diff --git a/AwsEncryptionSDK/runtimes/python/src/aws_encryption_sdk_dafny/internaldafny/generated/dafny_src-py.dtr b/AwsEncryptionSDK/runtimes/python/src/aws_encryption_sdk_dafny/internaldafny/generated/dafny_src-py.dtr new file mode 100644 index 000000000..db21452ce --- /dev/null +++ b/AwsEncryptionSDK/runtimes/python/src/aws_encryption_sdk_dafny/internaldafny/generated/dafny_src-py.dtr @@ -0,0 +1,59 @@ +file_format_version = "1.0" +dafny_version = "4.9.0.0" +[options_by_module.AwsCryptographyEncryptionSdkTypes] +legacy-module-names = false +python-module-name = "aws_encryption_sdk_dafny.internaldafny.generated" +[options_by_module.AbstractAwsCryptographyEncryptionSdkOperations] +legacy-module-names = false +python-module-name = "aws_encryption_sdk_dafny.internaldafny.generated" +[options_by_module.AbstractAwsCryptographyEncryptionSdkService] +legacy-module-names = false +python-module-name = "aws_encryption_sdk_dafny.internaldafny.generated" +[options_by_module.SerializableTypes] +legacy-module-names = false +python-module-name = "aws_encryption_sdk_dafny.internaldafny.generated" +[options_by_module.SerializeFunctions] +legacy-module-names = false +python-module-name = "aws_encryption_sdk_dafny.internaldafny.generated" +[options_by_module.EncryptionContext] +legacy-module-names = false +python-module-name = "aws_encryption_sdk_dafny.internaldafny.generated" +[options_by_module.HeaderTypes] +legacy-module-names = false +python-module-name = "aws_encryption_sdk_dafny.internaldafny.generated" +[options_by_module.SharedHeaderFunctions] +legacy-module-names = false +python-module-name = "aws_encryption_sdk_dafny.internaldafny.generated" +[options_by_module.EncryptedDataKeys] +legacy-module-names = false +python-module-name = "aws_encryption_sdk_dafny.internaldafny.generated" +[options_by_module.V1HeaderBody] +legacy-module-names = false +python-module-name = "aws_encryption_sdk_dafny.internaldafny.generated" +[options_by_module.V2HeaderBody] +legacy-module-names = false +python-module-name = "aws_encryption_sdk_dafny.internaldafny.generated" +[options_by_module.HeaderAuth] +legacy-module-names = false +python-module-name = "aws_encryption_sdk_dafny.internaldafny.generated" +[options_by_module.Header] +legacy-module-names = false +python-module-name = "aws_encryption_sdk_dafny.internaldafny.generated" +[options_by_module.Frames] +legacy-module-names = false +python-module-name = "aws_encryption_sdk_dafny.internaldafny.generated" +[options_by_module.MessageBody] +legacy-module-names = false +python-module-name = "aws_encryption_sdk_dafny.internaldafny.generated" +[options_by_module.KeyDerivation] +legacy-module-names = false +python-module-name = "aws_encryption_sdk_dafny.internaldafny.generated" +[options_by_module.EncryptDecryptHelpers] +legacy-module-names = false +python-module-name = "aws_encryption_sdk_dafny.internaldafny.generated" +[options_by_module.AwsEncryptionSdkOperations] +legacy-module-names = false +python-module-name = "aws_encryption_sdk_dafny.internaldafny.generated" +[options_by_module.ESDK] +legacy-module-names = false +python-module-name = "aws_encryption_sdk_dafny.internaldafny.generated" diff --git a/AwsEncryptionSDK/runtimes/python/src/aws_encryption_sdk_dafny/smithygenerated/aws_cryptography_encryptionsdk/__init__.py b/AwsEncryptionSDK/runtimes/python/src/aws_encryption_sdk_dafny/smithygenerated/aws_cryptography_encryptionsdk/__init__.py new file mode 100644 index 000000000..09be6133b --- /dev/null +++ b/AwsEncryptionSDK/runtimes/python/src/aws_encryption_sdk_dafny/smithygenerated/aws_cryptography_encryptionsdk/__init__.py @@ -0,0 +1,3 @@ +# Copyright Amazon.com Inc. or its affiliates. All Rights Reserved. +# SPDX-License-Identifier: Apache-2.0 +# Do not modify this file. This file is machine generated, and any changes to it will be overwritten. diff --git a/AwsEncryptionSDK/runtimes/python/src/aws_encryption_sdk_dafny/smithygenerated/aws_cryptography_encryptionsdk/client.py b/AwsEncryptionSDK/runtimes/python/src/aws_encryption_sdk_dafny/smithygenerated/aws_cryptography_encryptionsdk/client.py new file mode 100644 index 000000000..ef58389e8 --- /dev/null +++ b/AwsEncryptionSDK/runtimes/python/src/aws_encryption_sdk_dafny/smithygenerated/aws_cryptography_encryptionsdk/client.py @@ -0,0 +1,342 @@ +# Copyright Amazon.com Inc. or its affiliates. All Rights Reserved. +# SPDX-License-Identifier: Apache-2.0 +# Do not modify this file. This file is machine generated, and any changes to it will be overwritten. + +from aws_encryption_sdk_dafny.internaldafny.generated.AwsCryptographyEncryptionSdkTypes import ( + IAwsEncryptionSdkClient, +) +from typing import Callable, TypeVar, cast + +from .config import AwsEncryptionSdkConfig, Config +from .dafny_protocol import DafnyRequest, DafnyResponse +from .plugin import set_config_impl +from smithy_python.exceptions import SmithyRetryException +from smithy_python.interfaces.interceptor import Interceptor, InterceptorContext +from smithy_python.interfaces.retries import RetryErrorInfo, RetryErrorType + +from .config import Plugin +from .deserialize import _deserialize_decrypt, _deserialize_encrypt +from .errors import ServiceError +from .models import DecryptInput, DecryptOutput, EncryptInput, EncryptOutput +from .serialize import _serialize_decrypt, _serialize_encrypt + + +Input = TypeVar("Input") +Output = TypeVar("Output") + + +class AwsEncryptionSdk: + """Client for AwsEncryptionSdk. + + :param config: Configuration for the client. + """ + + def __init__( + self, + config: AwsEncryptionSdkConfig | None = None, + dafny_client: IAwsEncryptionSdkClient | None = None, + ): + if config is None: + self._config = Config() + else: + self._config = config + + client_plugins: list[Plugin] = [ + set_config_impl, + ] + + for plugin in client_plugins: + plugin(self._config) + + if dafny_client is not None: + self._config.dafnyImplInterface.impl = dafny_client + + def encrypt(self, input: EncryptInput) -> EncryptOutput: + """Invokes the Encrypt operation. + + :param input: The operation's input. + """ + return self._execute_operation( + input=input, + plugins=[], + serialize=_serialize_encrypt, + deserialize=_deserialize_encrypt, + config=self._config, + operation_name="Encrypt", + ) + + def decrypt(self, input: DecryptInput) -> DecryptOutput: + """Invokes the Decrypt operation. + + :param input: The operation's input. + """ + return self._execute_operation( + input=input, + plugins=[], + serialize=_serialize_decrypt, + deserialize=_deserialize_decrypt, + config=self._config, + operation_name="Decrypt", + ) + + def _execute_operation( + self, + input: Input, + plugins: list[Plugin], + serialize: Callable[[Input, Config], DafnyRequest], + deserialize: Callable[[DafnyResponse, Config], Output], + config: Config, + operation_name: str, + ) -> Output: + try: + return self._handle_execution( + input, plugins, serialize, deserialize, config, operation_name + ) + except Exception as e: + # Make sure every exception that we throw is an instance of ServiceError so + # customers can reliably catch everything we throw. + if not isinstance(e, ServiceError): + raise ServiceError(e) from e + raise e + + def _handle_execution( + self, + input: Input, + plugins: list[Plugin], + serialize: Callable[[Input, Config], DafnyRequest], + deserialize: Callable[[DafnyResponse, Config], Output], + config: Config, + operation_name: str, + ) -> Output: + context: InterceptorContext[Input, None, None, None] = InterceptorContext( + request=input, + response=None, + transport_request=None, + transport_response=None, + ) + _client_interceptors = config.interceptors + client_interceptors = cast( + list[Interceptor[Input, Output, DafnyRequest, DafnyResponse]], + _client_interceptors, + ) + interceptors = client_interceptors + + try: + # Step 1a: Invoke read_before_execution on client-level interceptors + for interceptor in client_interceptors: + interceptor.read_before_execution(context) + + # Step 1b: Run operation-level plugins + for plugin in plugins: + plugin(config) + + _client_interceptors = config.interceptors + interceptors = cast( + list[Interceptor[Input, Output, DafnyRequest, DafnyResponse]], + _client_interceptors, + ) + + # Step 1c: Invoke the read_before_execution hooks on newly added + # interceptors. + for interceptor in interceptors: + if interceptor not in client_interceptors: + interceptor.read_before_execution(context) + + # Step 2: Invoke the modify_before_serialization hooks + for interceptor in interceptors: + context._request = interceptor.modify_before_serialization(context) + + # Step 3: Invoke the read_before_serialization hooks + for interceptor in interceptors: + interceptor.read_before_serialization(context) + + # Step 4: Serialize the request + context_with_transport_request = cast( + InterceptorContext[Input, None, DafnyRequest, None], context + ) + context_with_transport_request._transport_request = serialize( + context_with_transport_request.request, config + ) + + # Step 5: Invoke read_after_serialization + for interceptor in interceptors: + interceptor.read_after_serialization(context_with_transport_request) + + # Step 6: Invoke modify_before_retry_loop + for interceptor in interceptors: + context_with_transport_request._transport_request = ( + interceptor.modify_before_retry_loop(context_with_transport_request) + ) + + # Step 7: Acquire the retry token. + retry_strategy = config.retry_strategy + retry_token = retry_strategy.acquire_initial_retry_token() + + while True: + # Make an attempt, creating a copy of the context so we don't pass + # around old data. + context_with_response = self._handle_attempt( + deserialize, + interceptors, + context_with_transport_request.copy(), + config, + operation_name, + ) + + # We perform this type-ignored re-assignment because `context` needs + # to point at the latest context so it can be generically handled + # later on. This is only an issue here because we've created a copy, + # so we're no longer simply pointing at the same object in memory + # with different names and type hints. It is possible to address this + # without having to fall back to the type ignore, but it would impose + # unnecessary runtime costs. + context = context_with_response # type: ignore + + if isinstance(context_with_response.response, Exception): + # Step 7u: Reacquire retry token if the attempt failed + try: + retry_token = retry_strategy.refresh_retry_token_for_retry( + token_to_renew=retry_token, + error_info=RetryErrorInfo( + # TODO: Determine the error type. + error_type=RetryErrorType.CLIENT_ERROR, + ), + ) + except SmithyRetryException: + raise context_with_response.response + else: + # Step 8: Invoke record_success + retry_strategy.record_success(token=retry_token) + break + except Exception as e: + context._response = e + + # At this point, the context's request will have been definitively set, and + # The response will be set either with the modeled output or an exception. The + # transport_request and transport_response may be set or None. + execution_context = cast( + InterceptorContext[ + Input, Output, DafnyRequest | None, DafnyResponse | None + ], + context, + ) + return self._finalize_execution(interceptors, execution_context) + + def _handle_attempt( + self, + deserialize: Callable[[DafnyResponse, Config], Output], + interceptors: list[Interceptor[Input, Output, DafnyRequest, DafnyResponse]], + context: InterceptorContext[Input, None, DafnyRequest, None], + config: Config, + operation_name: str, + ) -> InterceptorContext[Input, Output, DafnyRequest, DafnyResponse | None]: + try: + # Step 7a: Invoke read_before_attempt + for interceptor in interceptors: + interceptor.read_before_attempt(context) + + # Step 7m: Involve client Dafny impl + if config.dafnyImplInterface.impl is None: + raise Exception("No impl found on the operation config.") + + context_with_response = cast( + InterceptorContext[Input, None, DafnyRequest, DafnyResponse], context + ) + + context_with_response._transport_response = ( + config.dafnyImplInterface.handle_request( + input=context_with_response.transport_request + ) + ) + + # Step 7n: Invoke read_after_transmit + for interceptor in interceptors: + interceptor.read_after_transmit(context_with_response) + + # Step 7o: Invoke modify_before_deserialization + for interceptor in interceptors: + context_with_response._transport_response = ( + interceptor.modify_before_deserialization(context_with_response) + ) + + # Step 7p: Invoke read_before_deserialization + for interceptor in interceptors: + interceptor.read_before_deserialization(context_with_response) + + # Step 7q: deserialize + context_with_output = cast( + InterceptorContext[Input, Output, DafnyRequest, DafnyResponse], + context_with_response, + ) + context_with_output._response = deserialize( + context_with_output._transport_response, config + ) + + # Step 7r: Invoke read_after_deserialization + for interceptor in interceptors: + interceptor.read_after_deserialization(context_with_output) + except Exception as e: + context._response = e + + # At this point, the context's request and transport_request have definitively been set, + # the response is either set or an exception, and the transport_resposne is either set or + # None. This will also be true after _finalize_attempt because there is no opportunity + # there to set the transport_response. + attempt_context = cast( + InterceptorContext[Input, Output, DafnyRequest, DafnyResponse | None], + context, + ) + return self._finalize_attempt(interceptors, attempt_context) + + def _finalize_attempt( + self, + interceptors: list[Interceptor[Input, Output, DafnyRequest, DafnyResponse]], + context: InterceptorContext[Input, Output, DafnyRequest, DafnyResponse | None], + ) -> InterceptorContext[Input, Output, DafnyRequest, DafnyResponse | None]: + # Step 7s: Invoke modify_before_attempt_completion + try: + for interceptor in interceptors: + context._response = interceptor.modify_before_attempt_completion( + context + ) + except Exception as e: + context._response = e + + # Step 7t: Invoke read_after_attempt + for interceptor in interceptors: + try: + interceptor.read_after_attempt(context) + except Exception as e: + context._response = e + + return context + + def _finalize_execution( + self, + interceptors: list[Interceptor[Input, Output, DafnyRequest, DafnyResponse]], + context: InterceptorContext[ + Input, Output, DafnyRequest | None, DafnyResponse | None + ], + ) -> Output: + try: + # Step 9: Invoke modify_before_completion + for interceptor in interceptors: + context._response = interceptor.modify_before_completion(context) + + except Exception as e: + context._response = e + + # Step 11: Invoke read_after_execution + for interceptor in interceptors: + try: + interceptor.read_after_execution(context) + except Exception as e: + context._response = e + + # Step 12: Return / throw + if isinstance(context.response, Exception): + raise context.response + + # We may want to add some aspects of this context to the output types so we can + # return it to the end-users. + return context.response diff --git a/AwsEncryptionSDK/runtimes/python/src/aws_encryption_sdk_dafny/smithygenerated/aws_cryptography_encryptionsdk/config.py b/AwsEncryptionSDK/runtimes/python/src/aws_encryption_sdk_dafny/smithygenerated/aws_cryptography_encryptionsdk/config.py new file mode 100644 index 000000000..efa756c2d --- /dev/null +++ b/AwsEncryptionSDK/runtimes/python/src/aws_encryption_sdk_dafny/smithygenerated/aws_cryptography_encryptionsdk/config.py @@ -0,0 +1,150 @@ +# Copyright Amazon.com Inc. or its affiliates. All Rights Reserved. +# SPDX-License-Identifier: Apache-2.0 +# Do not modify this file. This file is machine generated, and any changes to it will be overwritten. + +from aws_encryption_sdk_dafny.internaldafny.generated.AwsCryptographyEncryptionSdkTypes import ( + AwsEncryptionSdkConfig_AwsEncryptionSdkConfig as DafnyAwsEncryptionSdkConfig, +) +import aws_encryption_sdk_dafny.internaldafny.generated.module_ +import aws_encryption_sdk_dafny.smithygenerated.aws_cryptography_encryptionsdk.dafny_to_smithy +import aws_encryption_sdk_dafny.smithygenerated.aws_cryptography_encryptionsdk.smithy_to_dafny +from dataclasses import dataclass +from typing import Any, Callable, Dict, Optional, TypeAlias + +from .dafnyImplInterface import DafnyImplInterface +from smithy_python._private.retries import SimpleRetryStrategy +from smithy_python.interfaces.retries import RetryStrategy + + +_ServiceInterceptor = Any + + +@dataclass(init=False) +class Config: + """Configuration for AwsEncryptionSdk.""" + + interceptors: list[_ServiceInterceptor] + retry_strategy: RetryStrategy + dafnyImplInterface: DafnyImplInterface | None + + def __init__( + self, + *, + interceptors: list[_ServiceInterceptor] | None = None, + retry_strategy: RetryStrategy | None = None, + dafnyImplInterface: DafnyImplInterface | None = None, + ): + """Constructor. + + :param interceptors: The list of interceptors, which are hooks + that are called during the execution of a request. + :param retry_strategy: The retry strategy for issuing retry + tokens and computing retry delays. + :param dafnyImplInterface: + """ + self.interceptors = interceptors or [] + self.retry_strategy = retry_strategy or SimpleRetryStrategy() + self.dafnyImplInterface = dafnyImplInterface + + +# A callable that allows customizing the config object on each request. +Plugin: TypeAlias = Callable[[Config], None] + + +class AwsEncryptionSdkConfig(Config): + commitment_policy: Optional[str] + max_encrypted_data_keys: int + net_v4_0_0_retry_policy: Optional[str] + + def __init__( + self, + *, + commitment_policy: Optional[str] = None, + max_encrypted_data_keys: int = 0, + net_v4_0_0_retry_policy: Optional[str] = None, + ): + """Constructor for AwsEncryptionSdkConfig. + + :param net_v4_0_0_retry_policy: During Decryption, Allow or + Forbid ESDK-NET v4.0.0 Behavior if the ESDK Message Header + fails the Header Authentication check. + """ + super().__init__() + self.commitment_policy = commitment_policy + if (max_encrypted_data_keys is not None) and (max_encrypted_data_keys < 1): + raise ValueError( + "max_encrypted_data_keys must be greater than or equal to 1" + ) + + self.max_encrypted_data_keys = max_encrypted_data_keys + self.net_v4_0_0_retry_policy = net_v4_0_0_retry_policy + + def as_dict(self) -> Dict[str, Any]: + """Converts the AwsEncryptionSdkConfig to a dictionary.""" + d: Dict[str, Any] = {} + + if self.commitment_policy is not None: + d["commitment_policy"] = self.commitment_policy + + if self.max_encrypted_data_keys is not None: + d["max_encrypted_data_keys"] = self.max_encrypted_data_keys + + if self.net_v4_0_0_retry_policy is not None: + d["net_v4_0_0_retry_policy"] = self.net_v4_0_0_retry_policy + + return d + + @staticmethod + def from_dict(d: Dict[str, Any]) -> "AwsEncryptionSdkConfig": + """Creates a AwsEncryptionSdkConfig from a dictionary.""" + kwargs: Dict[str, Any] = {} + + if "commitment_policy" in d: + kwargs["commitment_policy"] = d["commitment_policy"] + + if "max_encrypted_data_keys" in d: + kwargs["max_encrypted_data_keys"] = d["max_encrypted_data_keys"] + + if "net_v4_0_0_retry_policy" in d: + kwargs["net_v4_0_0_retry_policy"] = d["net_v4_0_0_retry_policy"] + + return AwsEncryptionSdkConfig(**kwargs) + + def __repr__(self) -> str: + result = "AwsEncryptionSdkConfig(" + if self.commitment_policy is not None: + result += f"commitment_policy={repr(self.commitment_policy)}, " + + if self.max_encrypted_data_keys is not None: + result += f"max_encrypted_data_keys={repr(self.max_encrypted_data_keys)}, " + + if self.net_v4_0_0_retry_policy is not None: + result += f"net_v4_0_0_retry_policy={repr(self.net_v4_0_0_retry_policy)}" + + return result + ")" + + def __eq__(self, other: Any) -> bool: + if not isinstance(other, AwsEncryptionSdkConfig): + return False + attributes: list[str] = [ + "commitment_policy", + "max_encrypted_data_keys", + "net_v4_0_0_retry_policy", + ] + return all(getattr(self, a) == getattr(other, a) for a in attributes) + + +def dafny_config_to_smithy_config(dafny_config) -> AwsEncryptionSdkConfig: + """Converts the provided Dafny shape for this localService's config into + the corresponding Smithy-modelled shape.""" + return aws_encryption_sdk_dafny.smithygenerated.aws_cryptography_encryptionsdk.dafny_to_smithy.aws_cryptography_encryptionsdk_AwsEncryptionSdkConfig( + dafny_config + ) + + +def smithy_config_to_dafny_config(smithy_config) -> DafnyAwsEncryptionSdkConfig: + """Converts the provided Smithy-modelled shape for this localService's + config into the corresponding Dafny shape.""" + return aws_encryption_sdk_dafny.smithygenerated.aws_cryptography_encryptionsdk.smithy_to_dafny.aws_cryptography_encryptionsdk_AwsEncryptionSdkConfig( + smithy_config + ) diff --git a/AwsEncryptionSDK/runtimes/python/src/aws_encryption_sdk_dafny/smithygenerated/aws_cryptography_encryptionsdk/dafnyImplInterface.py b/AwsEncryptionSDK/runtimes/python/src/aws_encryption_sdk_dafny/smithygenerated/aws_cryptography_encryptionsdk/dafnyImplInterface.py new file mode 100644 index 000000000..bce3e7bba --- /dev/null +++ b/AwsEncryptionSDK/runtimes/python/src/aws_encryption_sdk_dafny/smithygenerated/aws_cryptography_encryptionsdk/dafnyImplInterface.py @@ -0,0 +1,32 @@ +# Copyright Amazon.com Inc. or its affiliates. All Rights Reserved. +# SPDX-License-Identifier: Apache-2.0 +# Do not modify this file. This file is machine generated, and any changes to it will be overwritten. + +from aws_encryption_sdk_dafny.internaldafny.generated.ESDK import ESDKClient +from .dafny_protocol import DafnyRequest + + +class DafnyImplInterface: + impl: ESDKClient | None = None + + # operation_map cannot be created at dafnyImplInterface create time, + # as the map's values reference values inside `self.impl`, + # and impl is only populated at runtime. + # Accessing these before impl is populated results in an error. + # At runtime, the map is populated once and cached. + operation_map = None + + def handle_request(self, input: DafnyRequest): + if self.operation_map is None: + self.operation_map = { + "Encrypt": self.impl.Encrypt, + "Decrypt": self.impl.Decrypt, + } + + # This logic is where a typical Smithy client would expect the "server" to be. + # This code can be thought of as logic our Dafny "server" uses + # to route incoming client requests to the correct request handler code. + if input.dafny_operation_input is None: + return self.operation_map[input.operation_name]() + else: + return self.operation_map[input.operation_name](input.dafny_operation_input) diff --git a/AwsEncryptionSDK/runtimes/python/src/aws_encryption_sdk_dafny/smithygenerated/aws_cryptography_encryptionsdk/dafny_protocol.py b/AwsEncryptionSDK/runtimes/python/src/aws_encryption_sdk_dafny/smithygenerated/aws_cryptography_encryptionsdk/dafny_protocol.py new file mode 100644 index 000000000..954ce7987 --- /dev/null +++ b/AwsEncryptionSDK/runtimes/python/src/aws_encryption_sdk_dafny/smithygenerated/aws_cryptography_encryptionsdk/dafny_protocol.py @@ -0,0 +1,33 @@ +# Copyright Amazon.com Inc. or its affiliates. All Rights Reserved. +# SPDX-License-Identifier: Apache-2.0 +# Do not modify this file. This file is machine generated, and any changes to it will be overwritten. + +from aws_encryption_sdk_dafny.internaldafny.generated.AwsCryptographyEncryptionSdkTypes import ( + DecryptInput_DecryptInput as DafnyDecryptInput, + EncryptInput_EncryptInput as DafnyEncryptInput, +) +import aws_encryption_sdk_dafny.internaldafny.generated.module_ + + +import smithy_dafny_standard_library.internaldafny.generated.Wrappers as Wrappers +from typing import Union + + +class DafnyRequest: + operation_name: str + + # dafny_operation_input can take on any one of the types + # of the input values passed to the Dafny implementation + dafny_operation_input: Union[ + DafnyEncryptInput, + DafnyDecryptInput, + ] + + def __init__(self, operation_name, dafny_operation_input): + self.operation_name = operation_name + self.dafny_operation_input = dafny_operation_input + + +class DafnyResponse(Wrappers.Result): + def __init__(self): + super().__init__(self) diff --git a/AwsEncryptionSDK/runtimes/python/src/aws_encryption_sdk_dafny/smithygenerated/aws_cryptography_encryptionsdk/dafny_to_smithy.py b/AwsEncryptionSDK/runtimes/python/src/aws_encryption_sdk_dafny/smithygenerated/aws_cryptography_encryptionsdk/dafny_to_smithy.py new file mode 100644 index 000000000..f0e1608d7 --- /dev/null +++ b/AwsEncryptionSDK/runtimes/python/src/aws_encryption_sdk_dafny/smithygenerated/aws_cryptography_encryptionsdk/dafny_to_smithy.py @@ -0,0 +1,182 @@ +# Copyright Amazon.com Inc. or its affiliates. All Rights Reserved. +# SPDX-License-Identifier: Apache-2.0 +# Do not modify this file. This file is machine generated, and any changes to it will be overwritten. + +import aws_cryptographic_material_providers.smithygenerated.aws_cryptography_materialproviders.dafny_to_smithy +from aws_encryption_sdk_dafny.internaldafny.generated.AwsCryptographyEncryptionSdkTypes import ( + NetV4__0__0__RetryPolicy_ALLOW__RETRY, + NetV4__0__0__RetryPolicy_FORBID__RETRY, +) +import aws_encryption_sdk_dafny.internaldafny.generated.module_ +import aws_encryption_sdk_dafny.smithygenerated.aws_cryptography_encryptionsdk.dafny_to_smithy +import aws_encryption_sdk_dafny.smithygenerated.aws_cryptography_encryptionsdk.models + + +def aws_cryptography_encryptionsdk_EncryptInput(dafny_input): + return aws_encryption_sdk_dafny.smithygenerated.aws_cryptography_encryptionsdk.models.EncryptInput( + plaintext=bytes(dafny_input.plaintext), + encryption_context=( + ( + { + bytes(key.Elements) + .decode("utf-8"): bytes(value.Elements) + .decode("utf-8") + for (key, value) in dafny_input.encryptionContext.value.items + } + ) + if (dafny_input.encryptionContext.is_Some) + else None + ), + materials_manager=( + ( + aws_cryptographic_material_providers.smithygenerated.aws_cryptography_materialproviders.dafny_to_smithy.aws_cryptography_materialproviders_CryptographicMaterialsManagerReference( + dafny_input.materialsManager.UnwrapOr(None) + ) + ) + if (dafny_input.materialsManager.UnwrapOr(None) is not None) + else None + ), + keyring=( + ( + aws_cryptographic_material_providers.smithygenerated.aws_cryptography_materialproviders.dafny_to_smithy.aws_cryptography_materialproviders_KeyringReference( + dafny_input.keyring.UnwrapOr(None) + ) + ) + if (dafny_input.keyring.UnwrapOr(None) is not None) + else None + ), + algorithm_suite_id=( + ( + aws_cryptographic_material_providers.smithygenerated.aws_cryptography_materialproviders.dafny_to_smithy.aws_cryptography_materialproviders_ESDKAlgorithmSuiteId( + dafny_input.algorithmSuiteId.value + ) + ) + if (dafny_input.algorithmSuiteId.is_Some) + else None + ), + frame_length=( + (dafny_input.frameLength.value) + if (dafny_input.frameLength.is_Some) + else None + ), + ) + + +def aws_cryptography_encryptionsdk_DecryptInput(dafny_input): + return aws_encryption_sdk_dafny.smithygenerated.aws_cryptography_encryptionsdk.models.DecryptInput( + ciphertext=bytes(dafny_input.ciphertext), + materials_manager=( + ( + aws_cryptographic_material_providers.smithygenerated.aws_cryptography_materialproviders.dafny_to_smithy.aws_cryptography_materialproviders_CryptographicMaterialsManagerReference( + dafny_input.materialsManager.UnwrapOr(None) + ) + ) + if (dafny_input.materialsManager.UnwrapOr(None) is not None) + else None + ), + keyring=( + ( + aws_cryptographic_material_providers.smithygenerated.aws_cryptography_materialproviders.dafny_to_smithy.aws_cryptography_materialproviders_KeyringReference( + dafny_input.keyring.UnwrapOr(None) + ) + ) + if (dafny_input.keyring.UnwrapOr(None) is not None) + else None + ), + encryption_context=( + ( + { + bytes(key.Elements) + .decode("utf-8"): bytes(value.Elements) + .decode("utf-8") + for (key, value) in dafny_input.encryptionContext.value.items + } + ) + if (dafny_input.encryptionContext.is_Some) + else None + ), + ) + + +def aws_cryptography_encryptionsdk_EncryptOutput(dafny_input): + return aws_encryption_sdk_dafny.smithygenerated.aws_cryptography_encryptionsdk.models.EncryptOutput( + ciphertext=bytes(dafny_input.ciphertext), + encryption_context={ + bytes(key.Elements).decode("utf-8"): bytes(value.Elements).decode("utf-8") + for (key, value) in dafny_input.encryptionContext.items + }, + algorithm_suite_id=aws_cryptographic_material_providers.smithygenerated.aws_cryptography_materialproviders.dafny_to_smithy.aws_cryptography_materialproviders_ESDKAlgorithmSuiteId( + dafny_input.algorithmSuiteId + ), + ) + + +def aws_cryptography_encryptionsdk_DecryptOutput(dafny_input): + return aws_encryption_sdk_dafny.smithygenerated.aws_cryptography_encryptionsdk.models.DecryptOutput( + plaintext=bytes(dafny_input.plaintext), + encryption_context={ + bytes(key.Elements).decode("utf-8"): bytes(value.Elements).decode("utf-8") + for (key, value) in dafny_input.encryptionContext.items + }, + algorithm_suite_id=aws_cryptographic_material_providers.smithygenerated.aws_cryptography_materialproviders.dafny_to_smithy.aws_cryptography_materialproviders_ESDKAlgorithmSuiteId( + dafny_input.algorithmSuiteId + ), + ) + + +def aws_cryptography_encryptionsdk_AtomicPrimitivesReference(dafny_input): + from aws_cryptography_primitives.smithygenerated.aws_cryptography_primitives.client import ( + AwsCryptographicPrimitives, + ) + + return AwsCryptographicPrimitives(config=None, dafny_client=dafny_input) + + +def aws_cryptography_encryptionsdk_NetV4_0_0_RetryPolicy(dafny_input): + if isinstance(dafny_input, NetV4__0__0__RetryPolicy_FORBID__RETRY): + return "FORBID_RETRY" + + elif isinstance(dafny_input, NetV4__0__0__RetryPolicy_ALLOW__RETRY): + return "ALLOW_RETRY" + + else: + raise ValueError(f"No recognized enum value in enum type: {dafny_input=}") + + +def aws_cryptography_encryptionsdk_AwsEncryptionSdkConfig(dafny_input): + # Deferred import of .config to avoid circular dependency + import aws_encryption_sdk_dafny.smithygenerated.aws_cryptography_encryptionsdk.config + + return aws_encryption_sdk_dafny.smithygenerated.aws_cryptography_encryptionsdk.config.AwsEncryptionSdkConfig( + commitment_policy=( + ( + aws_cryptographic_material_providers.smithygenerated.aws_cryptography_materialproviders.dafny_to_smithy.aws_cryptography_materialproviders_ESDKCommitmentPolicy( + dafny_input.commitmentPolicy.value + ) + ) + if (dafny_input.commitmentPolicy.is_Some) + else None + ), + max_encrypted_data_keys=( + (dafny_input.maxEncryptedDataKeys.value) + if (dafny_input.maxEncryptedDataKeys.is_Some) + else None + ), + net_v4_0_0_retry_policy=( + ( + aws_encryption_sdk_dafny.smithygenerated.aws_cryptography_encryptionsdk.dafny_to_smithy.aws_cryptography_encryptionsdk_NetV4_0_0_RetryPolicy( + dafny_input.netV4__0__0__RetryPolicy.value + ) + ) + if (dafny_input.netV4__0__0__RetryPolicy.is_Some) + else None + ), + ) + + +def aws_cryptography_encryptionsdk_MaterialProvidersReference(dafny_input): + from aws_cryptographic_material_providers.smithygenerated.aws_cryptography_materialproviders.client import ( + AwsCryptographicMaterialProviders, + ) + + return AwsCryptographicMaterialProviders(config=None, dafny_client=dafny_input) diff --git a/AwsEncryptionSDK/runtimes/python/src/aws_encryption_sdk_dafny/smithygenerated/aws_cryptography_encryptionsdk/deserialize.py b/AwsEncryptionSDK/runtimes/python/src/aws_encryption_sdk_dafny/smithygenerated/aws_cryptography_encryptionsdk/deserialize.py new file mode 100644 index 000000000..8788cea7c --- /dev/null +++ b/AwsEncryptionSDK/runtimes/python/src/aws_encryption_sdk_dafny/smithygenerated/aws_cryptography_encryptionsdk/deserialize.py @@ -0,0 +1,78 @@ +# Copyright Amazon.com Inc. or its affiliates. All Rights Reserved. +# SPDX-License-Identifier: Apache-2.0 +# Do not modify this file. This file is machine generated, and any changes to it will be overwritten. + +import _dafny +from aws_encryption_sdk_dafny.internaldafny.generated.AwsCryptographyEncryptionSdkTypes import ( + DecryptOutput_DecryptOutput as DafnyDecryptOutput, + EncryptOutput_EncryptOutput as DafnyEncryptOutput, + Error, + Error_AwsEncryptionSdkException, +) +import aws_encryption_sdk_dafny.internaldafny.generated.module_ +import aws_encryption_sdk_dafny.smithygenerated.aws_cryptography_encryptionsdk.dafny_to_smithy +from typing import Any + +from .dafny_protocol import DafnyResponse +from .errors import ( + AwsCryptographicMaterialProviders, + AwsCryptographicPrimitives, + AwsEncryptionSdkException, + CollectionOfErrors, + OpaqueError, + ServiceError, +) +from aws_cryptographic_material_providers.smithygenerated.aws_cryptography_materialproviders.deserialize import ( + _deserialize_error as aws_cryptography_materialproviders_deserialize_error, +) +from aws_cryptography_primitives.smithygenerated.aws_cryptography_primitives.deserialize import ( + _deserialize_error as aws_cryptography_primitives_deserialize_error, +) + +from .config import Config + + +def _deserialize_encrypt(input: DafnyResponse, config: Config): + + if input.IsFailure(): + return _deserialize_error(input.error) + return aws_encryption_sdk_dafny.smithygenerated.aws_cryptography_encryptionsdk.dafny_to_smithy.aws_cryptography_encryptionsdk_EncryptOutput( + input.value + ) + + +def _deserialize_decrypt(input: DafnyResponse, config: Config): + + if input.IsFailure(): + return _deserialize_error(input.error) + return aws_encryption_sdk_dafny.smithygenerated.aws_cryptography_encryptionsdk.dafny_to_smithy.aws_cryptography_encryptionsdk_DecryptOutput( + input.value + ) + + +def _deserialize_error(error: Error) -> ServiceError: + if error.is_Opaque: + return OpaqueError(obj=error.obj) + elif error.is_OpaqueWithText: + return OpaqueErrorWithText(obj=error.obj, obj_message=error.objMessage) + elif error.is_CollectionOfErrors: + return CollectionOfErrors( + message=_dafny.string_of(error.message), + list=[_deserialize_error(dafny_e) for dafny_e in error.list], + ) + elif error.is_AwsEncryptionSdkException: + return AwsEncryptionSdkException(message=_dafny.string_of(error.message)) + elif error.is_AwsCryptographyPrimitives: + return AwsCryptographicPrimitives( + aws_cryptography_primitives_deserialize_error( + error.AwsCryptographyPrimitives + ) + ) + elif error.is_AwsCryptographyMaterialProviders: + return AwsCryptographicMaterialProviders( + aws_cryptography_materialproviders_deserialize_error( + error.AwsCryptographyMaterialProviders + ) + ) + else: + return OpaqueError(obj=error) diff --git a/AwsEncryptionSDK/runtimes/python/src/aws_encryption_sdk_dafny/smithygenerated/aws_cryptography_encryptionsdk/errors.py b/AwsEncryptionSDK/runtimes/python/src/aws_encryption_sdk_dafny/smithygenerated/aws_cryptography_encryptionsdk/errors.py new file mode 100644 index 000000000..2947fbc12 --- /dev/null +++ b/AwsEncryptionSDK/runtimes/python/src/aws_encryption_sdk_dafny/smithygenerated/aws_cryptography_encryptionsdk/errors.py @@ -0,0 +1,303 @@ +# Copyright Amazon.com Inc. or its affiliates. All Rights Reserved. +# SPDX-License-Identifier: Apache-2.0 +# Do not modify this file. This file is machine generated, and any changes to it will be overwritten. + +import _dafny +from aws_cryptographic_material_providers.smithygenerated.aws_cryptography_materialproviders.errors import ( + _smithy_error_to_dafny_error as aws_cryptography_materialproviders_smithy_error_to_dafny_error, +) +from aws_cryptography_primitives.smithygenerated.aws_cryptography_primitives.errors import ( + _smithy_error_to_dafny_error as aws_cryptography_primitives_smithy_error_to_dafny_error, +) +import aws_encryption_sdk_dafny.internaldafny.generated +import aws_encryption_sdk_dafny.internaldafny.generated.AwsCryptographyEncryptionSdkTypes +import aws_encryption_sdk_dafny.smithygenerated.aws_cryptography_encryptionsdk.errors +from typing import Any, Dict, Generic, List, Literal, TypeVar + + +class ServiceError(Exception): + """Base error for all errors in the service.""" + + pass + + +T = TypeVar("T") + + +class ApiError(ServiceError, Generic[T]): + """Base error for all api errors in the service.""" + + code: T + + def __init__(self, message: str): + super().__init__(message) + self.message = message + + +class UnknownApiError(ApiError[Literal["Unknown"]]): + """Error representing any unknown api errors.""" + + code: Literal["Unknown"] = "Unknown" + + +class AwsEncryptionSdkException(ApiError[Literal["AwsEncryptionSdkException"]]): + code: Literal["AwsEncryptionSdkException"] = "AwsEncryptionSdkException" + message: str + + def __init__( + self, + *, + message: str, + ): + super().__init__(message) + + def as_dict(self) -> Dict[str, Any]: + """Converts the AwsEncryptionSdkException to a dictionary.""" + return { + "message": self.message, + "code": self.code, + } + + @staticmethod + def from_dict(d: Dict[str, Any]) -> "AwsEncryptionSdkException": + """Creates a AwsEncryptionSdkException from a dictionary.""" + kwargs: Dict[str, Any] = { + "message": d["message"], + } + + return AwsEncryptionSdkException(**kwargs) + + def __repr__(self) -> str: + result = "AwsEncryptionSdkException(" + if self.message is not None: + result += f"message={repr(self.message)}" + + return result + ")" + + def __eq__(self, other: Any) -> bool: + if not isinstance(other, AwsEncryptionSdkException): + return False + attributes: list[str] = [ + "message", + "message", + ] + return all(getattr(self, a) == getattr(other, a) for a in attributes) + + +class AwsEncryptionSdkException(ApiError[Literal["AwsEncryptionSdkException"]]): + code: Literal["AwsEncryptionSdkException"] = "AwsEncryptionSdkException" + message: str + + +class AwsCryptographicPrimitives(ApiError[Literal["AwsCryptographicPrimitives"]]): + AwsCryptographicPrimitives: Any + + +class AwsCryptographicMaterialProviders( + ApiError[Literal["AwsCryptographicMaterialProviders"]] +): + AwsCryptographicMaterialProviders: Any + + +class CollectionOfErrors(ApiError[Literal["CollectionOfErrors"]]): + code: Literal["CollectionOfErrors"] = "CollectionOfErrors" + message: str + list: List[ServiceError] + + def __init__(self, *, message: str, list): + super().__init__(message) + self.list = list + + def as_dict(self) -> Dict[str, Any]: + """Converts the CollectionOfErrors to a dictionary. + + The dictionary uses the modeled shape names rather than the + parameter names as keys to be mostly compatible with boto3. + """ + return { + "message": self.message, + "code": self.code, + "list": self.list, + } + + @staticmethod + def from_dict(d: Dict[str, Any]) -> "CollectionOfErrors": + """Creates a CollectionOfErrors from a dictionary. + + The dictionary is expected to use the modeled shape names rather + than the parameter names as keys to be mostly compatible with + boto3. + """ + kwargs: Dict[str, Any] = {"message": d["message"], "list": d["list"]} + + return CollectionOfErrors(**kwargs) + + def __repr__(self) -> str: + result = "CollectionOfErrors(" + result += f"message={self.message}," + if self.message is not None: + result += f"message={repr(self.message)}" + result += f"list={self.list}" + result += ")" + return result + + def __eq__(self, other: Any) -> bool: + if not isinstance(other, CollectionOfErrors): + return False + if not (self.list == other.list): + return False + attributes: list[str] = ["message", "message"] + return all(getattr(self, a) == getattr(other, a) for a in attributes) + + +class OpaqueError(ApiError[Literal["OpaqueError"]]): + code: Literal["OpaqueError"] = "OpaqueError" + obj: Any # As an OpaqueError, type of obj is unknown + + def __init__(self, *, obj): + super().__init__("") + self.obj = obj + + def as_dict(self) -> Dict[str, Any]: + """Converts the OpaqueError to a dictionary. + + The dictionary uses the modeled shape names rather than the + parameter names as keys to be mostly compatible with boto3. + """ + return { + "message": self.message, + "code": self.code, + "obj": self.obj, + } + + @staticmethod + def from_dict(d: Dict[str, Any]) -> "OpaqueError": + """Creates a OpaqueError from a dictionary. + + The dictionary is expected to use the modeled shape names rather + than the parameter names as keys to be mostly compatible with + boto3. + """ + kwargs: Dict[str, Any] = {"message": d["message"], "obj": d["obj"]} + + return OpaqueError(**kwargs) + + def __repr__(self) -> str: + result = "OpaqueError(" + result += f"message={self.message}," + if self.message is not None: + result += f"message={repr(self.message)}" + result += f"obj={self.obj}" + result += ")" + return result + + def __eq__(self, other: Any) -> bool: + if not isinstance(other, OpaqueError): + return False + if not (self.obj == other.obj): + return False + attributes: list[str] = ["message", "message"] + return all(getattr(self, a) == getattr(other, a) for a in attributes) + + +class OpaqueWithTextError(ApiError[Literal["OpaqueWithTextError"]]): + code: Literal["OpaqueWithTextError"] = "OpaqueWithTextError" + obj: Any # As an OpaqueWithTextError, type of obj is unknown + obj_message: str # obj_message is a message representing the details of obj + + def __init__(self, *, obj, obj_message): + super().__init__("") + self.obj = obj + self.obj_message = obj_message + + def as_dict(self) -> Dict[str, Any]: + """Converts the OpaqueWithTextError to a dictionary. + + The dictionary uses the modeled shape names rather than the + parameter names as keys to be mostly compatible with boto3. + """ + return { + "message": self.message, + "code": self.code, + "obj": self.obj, + "obj_message": self.obj_message, + } + + @staticmethod + def from_dict(d: Dict[str, Any]) -> "OpaqueWithTextError": + """Creates a OpaqueWithTextError from a dictionary. + + The dictionary is expected to use the modeled shape names rather + than the parameter names as keys to be mostly compatible with + boto3. + """ + kwargs: Dict[str, Any] = { + "message": d["message"], + "obj": d["obj"], + "obj_message": d["obj_message"], + } + + return OpaqueWithTextError(**kwargs) + + def __repr__(self) -> str: + result = "OpaqueWithTextError(" + result += f"message={self.message}," + if self.message is not None: + result += f"message={repr(self.message)}" + result += f"obj={self.obj}" + result += f"obj_message={self.obj_message}" + result += ")" + return result + + def __eq__(self, other: Any) -> bool: + if not isinstance(other, OpaqueWithTextError): + return False + if not (self.obj == other.obj): + return False + attributes: list[str] = ["message", "message"] + return all(getattr(self, a) == getattr(other, a) for a in attributes) + + +def _smithy_error_to_dafny_error(e: ServiceError): + """Converts the provided native Smithy-modeled error into the corresponding + Dafny error.""" + if isinstance( + e, + aws_encryption_sdk_dafny.smithygenerated.aws_cryptography_encryptionsdk.errors.AwsEncryptionSdkException, + ): + return aws_encryption_sdk_dafny.internaldafny.generated.AwsCryptographyEncryptionSdkTypes.Error_AwsEncryptionSdkException( + message=_dafny.Seq(e.message) + ) + + if isinstance(e, AwsCryptographicPrimitives): + return aws_encryption_sdk_dafny.internaldafny.generated.AwsCryptographyEncryptionSdkTypes.Error_AwsCryptographyPrimitives( + aws_cryptography_primitives_smithy_error_to_dafny_error(e.message) + ) + + if isinstance(e, AwsCryptographicMaterialProviders): + return aws_encryption_sdk_dafny.internaldafny.generated.AwsCryptographyEncryptionSdkTypes.Error_AwsCryptographyMaterialProviders( + aws_cryptography_materialproviders_smithy_error_to_dafny_error(e.message) + ) + + if isinstance(e, CollectionOfErrors): + return aws_encryption_sdk_dafny.internaldafny.generated.AwsCryptographyEncryptionSdkTypes.Error_CollectionOfErrors( + message=_dafny.Seq(e.message), + list=_dafny.Seq( + _smithy_error_to_dafny_error(native_err) for native_err in e.list + ), + ) + + if isinstance(e, OpaqueError): + return aws_encryption_sdk_dafny.internaldafny.generated.AwsCryptographyEncryptionSdkTypes.Error_Opaque( + obj=e.obj + ) + + if isinstance(e, OpaqueWithTextError): + return aws_encryption_sdk_dafny.internaldafny.generated.AwsCryptographyEncryptionSdkTypes.Error_OpaqueWithText( + obj=e.obj, objMessage=e.obj_message + ) + + else: + return aws_encryption_sdk_dafny.internaldafny.generated.AwsCryptographyEncryptionSdkTypes.Error_Opaque( + obj=e + ) diff --git a/AwsEncryptionSDK/runtimes/python/src/aws_encryption_sdk_dafny/smithygenerated/aws_cryptography_encryptionsdk/models.py b/AwsEncryptionSDK/runtimes/python/src/aws_encryption_sdk_dafny/smithygenerated/aws_cryptography_encryptionsdk/models.py new file mode 100644 index 000000000..8f37ce666 --- /dev/null +++ b/AwsEncryptionSDK/runtimes/python/src/aws_encryption_sdk_dafny/smithygenerated/aws_cryptography_encryptionsdk/models.py @@ -0,0 +1,371 @@ +# Copyright Amazon.com Inc. or its affiliates. All Rights Reserved. +# SPDX-License-Identifier: Apache-2.0 +# Do not modify this file. This file is machine generated, and any changes to it will be overwritten. + +import aws_cryptographic_material_providers.smithygenerated.aws_cryptography_materialproviders.references +from typing import Any, Dict, Optional + + +class DecryptInput: + ciphertext: bytes | bytearray + materials_manager: Optional[ + "aws_cryptographic_material_providers.smithygenerated.aws_cryptography_materialproviders.references.CryptographicMaterialsManager" + ] + keyring: Optional[ + "aws_cryptographic_material_providers.smithygenerated.aws_cryptography_materialproviders.references.Keyring" + ] + encryption_context: Optional[dict[str, str]] + + def __init__( + self, + *, + ciphertext: bytes | bytearray, + materials_manager: Optional[ + "aws_cryptographic_material_providers.smithygenerated.aws_cryptography_materialproviders.references.CryptographicMaterialsManager" + ] = None, + keyring: Optional[ + "aws_cryptographic_material_providers.smithygenerated.aws_cryptography_materialproviders.references.Keyring" + ] = None, + encryption_context: Optional[dict[str, str]] = None, + ): + self.ciphertext = ciphertext + self.materials_manager = materials_manager + self.keyring = keyring + self.encryption_context = encryption_context + + def as_dict(self) -> Dict[str, Any]: + """Converts the DecryptInput to a dictionary.""" + d: Dict[str, Any] = { + "ciphertext": self.ciphertext, + } + + if self.materials_manager is not None: + d["materials_manager"] = self.materials_manager.as_dict() + + if self.keyring is not None: + d["keyring"] = self.keyring.as_dict() + + if self.encryption_context is not None: + d["encryption_context"] = self.encryption_context + + return d + + @staticmethod + def from_dict(d: Dict[str, Any]) -> "DecryptInput": + """Creates a DecryptInput from a dictionary.""" + from aws_cryptographic_material_providers.smithygenerated.aws_cryptography_materialproviders.references import ( + CryptographicMaterialsManager, + ) + from aws_cryptographic_material_providers.smithygenerated.aws_cryptography_materialproviders.references import ( + Keyring, + ) + + kwargs: Dict[str, Any] = { + "ciphertext": d["ciphertext"], + } + + if "materials_manager" in d: + kwargs["materials_manager"] = CryptographicMaterialsManager.from_dict( + d["materials_manager"] + ) + + if "keyring" in d: + kwargs["keyring"] = Keyring.from_dict(d["keyring"]) + + if "encryption_context" in d: + kwargs["encryption_context"] = d["encryption_context"] + + return DecryptInput(**kwargs) + + def __repr__(self) -> str: + result = "DecryptInput(" + if self.ciphertext is not None: + result += f"ciphertext={repr(self.ciphertext)}, " + + if self.materials_manager is not None: + result += f"materials_manager={repr(self.materials_manager)}, " + + if self.keyring is not None: + result += f"keyring={repr(self.keyring)}, " + + if self.encryption_context is not None: + result += f"encryption_context={repr(self.encryption_context)}" + + return result + ")" + + def __eq__(self, other: Any) -> bool: + if not isinstance(other, DecryptInput): + return False + attributes: list[str] = [ + "ciphertext", + "materials_manager", + "keyring", + "encryption_context", + ] + return all(getattr(self, a) == getattr(other, a) for a in attributes) + + +class DecryptOutput: + plaintext: bytes | bytearray + encryption_context: dict[str, str] + algorithm_suite_id: str + + def __init__( + self, + *, + plaintext: bytes | bytearray, + encryption_context: dict[str, str], + algorithm_suite_id: str, + ): + self.plaintext = plaintext + self.encryption_context = encryption_context + self.algorithm_suite_id = algorithm_suite_id + + def as_dict(self) -> Dict[str, Any]: + """Converts the DecryptOutput to a dictionary.""" + return { + "plaintext": self.plaintext, + "encryption_context": self.encryption_context, + "algorithm_suite_id": self.algorithm_suite_id, + } + + @staticmethod + def from_dict(d: Dict[str, Any]) -> "DecryptOutput": + """Creates a DecryptOutput from a dictionary.""" + kwargs: Dict[str, Any] = { + "plaintext": d["plaintext"], + "encryption_context": d["encryption_context"], + "algorithm_suite_id": d["algorithm_suite_id"], + } + + return DecryptOutput(**kwargs) + + def __repr__(self) -> str: + result = "DecryptOutput(" + if self.plaintext is not None: + result += f"plaintext={repr(self.plaintext)}, " + + if self.encryption_context is not None: + result += f"encryption_context={repr(self.encryption_context)}, " + + if self.algorithm_suite_id is not None: + result += f"algorithm_suite_id={repr(self.algorithm_suite_id)}" + + return result + ")" + + def __eq__(self, other: Any) -> bool: + if not isinstance(other, DecryptOutput): + return False + attributes: list[str] = [ + "plaintext", + "encryption_context", + "algorithm_suite_id", + ] + return all(getattr(self, a) == getattr(other, a) for a in attributes) + + +class EncryptInput: + plaintext: bytes | bytearray + encryption_context: Optional[dict[str, str]] + materials_manager: Optional[ + "aws_cryptographic_material_providers.smithygenerated.aws_cryptography_materialproviders.references.CryptographicMaterialsManager" + ] + keyring: Optional[ + "aws_cryptographic_material_providers.smithygenerated.aws_cryptography_materialproviders.references.Keyring" + ] + algorithm_suite_id: Optional[str] + frame_length: int + + def __init__( + self, + *, + plaintext: bytes | bytearray, + encryption_context: Optional[dict[str, str]] = None, + materials_manager: Optional[ + "aws_cryptographic_material_providers.smithygenerated.aws_cryptography_materialproviders.references.CryptographicMaterialsManager" + ] = None, + keyring: Optional[ + "aws_cryptographic_material_providers.smithygenerated.aws_cryptography_materialproviders.references.Keyring" + ] = None, + algorithm_suite_id: Optional[str] = None, + frame_length: int = 0, + ): + self.plaintext = plaintext + self.encryption_context = encryption_context + self.materials_manager = materials_manager + self.keyring = keyring + self.algorithm_suite_id = algorithm_suite_id + if (frame_length is not None) and (frame_length < 1): + raise ValueError("frame_length must be greater than or equal to 1") + + if (frame_length is not None) and (frame_length > 4294967296): + raise ValueError("frame_length must be less than or equal to 4294967296") + + self.frame_length = frame_length + + def as_dict(self) -> Dict[str, Any]: + """Converts the EncryptInput to a dictionary.""" + d: Dict[str, Any] = { + "plaintext": self.plaintext, + } + + if self.encryption_context is not None: + d["encryption_context"] = self.encryption_context + + if self.materials_manager is not None: + d["materials_manager"] = self.materials_manager.as_dict() + + if self.keyring is not None: + d["keyring"] = self.keyring.as_dict() + + if self.algorithm_suite_id is not None: + d["algorithm_suite_id"] = self.algorithm_suite_id + + if self.frame_length is not None: + d["frame_length"] = self.frame_length + + return d + + @staticmethod + def from_dict(d: Dict[str, Any]) -> "EncryptInput": + """Creates a EncryptInput from a dictionary.""" + from aws_cryptographic_material_providers.smithygenerated.aws_cryptography_materialproviders.references import ( + CryptographicMaterialsManager, + ) + from aws_cryptographic_material_providers.smithygenerated.aws_cryptography_materialproviders.references import ( + Keyring, + ) + + kwargs: Dict[str, Any] = { + "plaintext": d["plaintext"], + } + + if "encryption_context" in d: + kwargs["encryption_context"] = d["encryption_context"] + + if "materials_manager" in d: + kwargs["materials_manager"] = CryptographicMaterialsManager.from_dict( + d["materials_manager"] + ) + + if "keyring" in d: + kwargs["keyring"] = Keyring.from_dict(d["keyring"]) + + if "algorithm_suite_id" in d: + kwargs["algorithm_suite_id"] = d["algorithm_suite_id"] + + if "frame_length" in d: + kwargs["frame_length"] = d["frame_length"] + + return EncryptInput(**kwargs) + + def __repr__(self) -> str: + result = "EncryptInput(" + if self.plaintext is not None: + result += f"plaintext={repr(self.plaintext)}, " + + if self.encryption_context is not None: + result += f"encryption_context={repr(self.encryption_context)}, " + + if self.materials_manager is not None: + result += f"materials_manager={repr(self.materials_manager)}, " + + if self.keyring is not None: + result += f"keyring={repr(self.keyring)}, " + + if self.algorithm_suite_id is not None: + result += f"algorithm_suite_id={repr(self.algorithm_suite_id)}, " + + if self.frame_length is not None: + result += f"frame_length={repr(self.frame_length)}" + + return result + ")" + + def __eq__(self, other: Any) -> bool: + if not isinstance(other, EncryptInput): + return False + attributes: list[str] = [ + "plaintext", + "encryption_context", + "materials_manager", + "keyring", + "algorithm_suite_id", + "frame_length", + ] + return all(getattr(self, a) == getattr(other, a) for a in attributes) + + +class EncryptOutput: + ciphertext: bytes | bytearray + encryption_context: dict[str, str] + algorithm_suite_id: str + + def __init__( + self, + *, + ciphertext: bytes | bytearray, + encryption_context: dict[str, str], + algorithm_suite_id: str, + ): + self.ciphertext = ciphertext + self.encryption_context = encryption_context + self.algorithm_suite_id = algorithm_suite_id + + def as_dict(self) -> Dict[str, Any]: + """Converts the EncryptOutput to a dictionary.""" + return { + "ciphertext": self.ciphertext, + "encryption_context": self.encryption_context, + "algorithm_suite_id": self.algorithm_suite_id, + } + + @staticmethod + def from_dict(d: Dict[str, Any]) -> "EncryptOutput": + """Creates a EncryptOutput from a dictionary.""" + kwargs: Dict[str, Any] = { + "ciphertext": d["ciphertext"], + "encryption_context": d["encryption_context"], + "algorithm_suite_id": d["algorithm_suite_id"], + } + + return EncryptOutput(**kwargs) + + def __repr__(self) -> str: + result = "EncryptOutput(" + if self.ciphertext is not None: + result += f"ciphertext={repr(self.ciphertext)}, " + + if self.encryption_context is not None: + result += f"encryption_context={repr(self.encryption_context)}, " + + if self.algorithm_suite_id is not None: + result += f"algorithm_suite_id={repr(self.algorithm_suite_id)}" + + return result + ")" + + def __eq__(self, other: Any) -> bool: + if not isinstance(other, EncryptOutput): + return False + attributes: list[str] = [ + "ciphertext", + "encryption_context", + "algorithm_suite_id", + ] + return all(getattr(self, a) == getattr(other, a) for a in attributes) + + +class NetV4_0_0_RetryPolicy: + """During Decryption, Allow or Forbid ESDK-NET v4.0.0 Behavior if the ESDK + Message Header fails the Header Authentication check.""" + + FORBID_RETRY = "FORBID_RETRY" + + ALLOW_RETRY = "ALLOW_RETRY" + + # This set contains every possible value known at the time this was generated. New + # values may be added in the future. + values = frozenset({"FORBID_RETRY", "ALLOW_RETRY"}) + + +class Unit: + pass diff --git a/AwsEncryptionSDK/runtimes/python/src/aws_encryption_sdk_dafny/smithygenerated/aws_cryptography_encryptionsdk/plugin.py b/AwsEncryptionSDK/runtimes/python/src/aws_encryption_sdk_dafny/smithygenerated/aws_cryptography_encryptionsdk/plugin.py new file mode 100644 index 000000000..8c2f1f329 --- /dev/null +++ b/AwsEncryptionSDK/runtimes/python/src/aws_encryption_sdk_dafny/smithygenerated/aws_cryptography_encryptionsdk/plugin.py @@ -0,0 +1,49 @@ +# Copyright Amazon.com Inc. or its affiliates. All Rights Reserved. +# SPDX-License-Identifier: Apache-2.0 +# Do not modify this file. This file is machine generated, and any changes to it will be overwritten. + +from .config import ( + Config, + Plugin, + smithy_config_to_dafny_config, + AwsEncryptionSdkConfig, +) +from smithy_python.interfaces.retries import RetryStrategy +from smithy_python.exceptions import SmithyRetryException +from .dafnyImplInterface import DafnyImplInterface + + +def set_config_impl(config: Config): + """Set the Dafny-compiled implementation in the Smithy-Python client Config + and load our custom NoRetriesStrategy.""" + config.dafnyImplInterface = DafnyImplInterface() + if isinstance(config, AwsEncryptionSdkConfig): + from aws_encryption_sdk_dafny.internaldafny.generated.ESDK import default__ + + config.dafnyImplInterface.impl = default__.ESDK( + smithy_config_to_dafny_config(config) + ).value + config.retry_strategy = NoRetriesStrategy() + + +class ZeroRetryDelayToken: + """Placeholder class required by Smithy-Python client implementation. + + Do not wait to retry. + """ + + retry_delay = 0 + + +class NoRetriesStrategy(RetryStrategy): + """Placeholder class required by Smithy-Python client implementation. + + Do not retry calling Dafny code. + """ + + def acquire_initial_retry_token(self): + return ZeroRetryDelayToken() + + def refresh_retry_token_for_retry(self, token_to_renew, error_info): + # Do not retry + raise SmithyRetryException() diff --git a/AwsEncryptionSDK/runtimes/python/src/aws_encryption_sdk_dafny/smithygenerated/aws_cryptography_encryptionsdk/serialize.py b/AwsEncryptionSDK/runtimes/python/src/aws_encryption_sdk_dafny/smithygenerated/aws_cryptography_encryptionsdk/serialize.py new file mode 100644 index 000000000..bc7b6a45f --- /dev/null +++ b/AwsEncryptionSDK/runtimes/python/src/aws_encryption_sdk_dafny/smithygenerated/aws_cryptography_encryptionsdk/serialize.py @@ -0,0 +1,27 @@ +# Copyright Amazon.com Inc. or its affiliates. All Rights Reserved. +# SPDX-License-Identifier: Apache-2.0 +# Do not modify this file. This file is machine generated, and any changes to it will be overwritten. + +import aws_encryption_sdk_dafny.smithygenerated.aws_cryptography_encryptionsdk.smithy_to_dafny + +from .dafny_protocol import DafnyRequest + +from .config import Config + + +def _serialize_encrypt(input, config: Config) -> DafnyRequest: + return DafnyRequest( + operation_name="Encrypt", + dafny_operation_input=aws_encryption_sdk_dafny.smithygenerated.aws_cryptography_encryptionsdk.smithy_to_dafny.aws_cryptography_encryptionsdk_EncryptInput( + input + ), + ) + + +def _serialize_decrypt(input, config: Config) -> DafnyRequest: + return DafnyRequest( + operation_name="Decrypt", + dafny_operation_input=aws_encryption_sdk_dafny.smithygenerated.aws_cryptography_encryptionsdk.smithy_to_dafny.aws_cryptography_encryptionsdk_DecryptInput( + input + ), + ) diff --git a/AwsEncryptionSDK/runtimes/python/src/aws_encryption_sdk_dafny/smithygenerated/aws_cryptography_encryptionsdk/smithy_to_dafny.py b/AwsEncryptionSDK/runtimes/python/src/aws_encryption_sdk_dafny/smithygenerated/aws_cryptography_encryptionsdk/smithy_to_dafny.py new file mode 100644 index 000000000..26cd700ae --- /dev/null +++ b/AwsEncryptionSDK/runtimes/python/src/aws_encryption_sdk_dafny/smithygenerated/aws_cryptography_encryptionsdk/smithy_to_dafny.py @@ -0,0 +1,234 @@ +# Copyright Amazon.com Inc. or its affiliates. All Rights Reserved. +# SPDX-License-Identifier: Apache-2.0 +# Do not modify this file. This file is machine generated, and any changes to it will be overwritten. + +from _dafny import Map, Seq +import aws_cryptographic_material_providers.smithygenerated.aws_cryptography_materialproviders.smithy_to_dafny +from aws_encryption_sdk_dafny.internaldafny.generated.AwsCryptographyEncryptionSdkTypes import ( + AwsEncryptionSdkConfig_AwsEncryptionSdkConfig as DafnyAwsEncryptionSdkConfig, + DecryptInput_DecryptInput as DafnyDecryptInput, + DecryptOutput_DecryptOutput as DafnyDecryptOutput, + EncryptInput_EncryptInput as DafnyEncryptInput, + EncryptOutput_EncryptOutput as DafnyEncryptOutput, + NetV4__0__0__RetryPolicy_ALLOW__RETRY, + NetV4__0__0__RetryPolicy_FORBID__RETRY, +) +import aws_encryption_sdk_dafny.internaldafny.generated.module_ +import aws_encryption_sdk_dafny.smithygenerated.aws_cryptography_encryptionsdk.smithy_to_dafny +from smithy_dafny_standard_library.internaldafny.generated.Wrappers import ( + Option_None, + Option_Some, +) + + +def aws_cryptography_encryptionsdk_EncryptInput(native_input): + return DafnyEncryptInput( + plaintext=Seq(native_input.plaintext), + encryptionContext=( + ( + Option_Some( + Map( + { + Seq(key.encode("utf-8")): Seq(value.encode("utf-8")) + for (key, value) in native_input.encryption_context.items() + } + ) + ) + ) + if (native_input.encryption_context is not None) + else (Option_None()) + ), + materialsManager=( + ( + Option_Some( + aws_cryptographic_material_providers.smithygenerated.aws_cryptography_materialproviders.smithy_to_dafny.aws_cryptography_materialproviders_CryptographicMaterialsManagerReference( + native_input.materials_manager + ) + ) + ) + if ( + (native_input.materials_manager is not None) + and ( + aws_cryptographic_material_providers.smithygenerated.aws_cryptography_materialproviders.smithy_to_dafny.aws_cryptography_materialproviders_CryptographicMaterialsManagerReference( + native_input.materials_manager + ) + is not None + ) + ) + else (Option_None()) + ), + keyring=( + ( + Option_Some( + aws_cryptographic_material_providers.smithygenerated.aws_cryptography_materialproviders.smithy_to_dafny.aws_cryptography_materialproviders_KeyringReference( + native_input.keyring + ) + ) + ) + if ( + (native_input.keyring is not None) + and ( + aws_cryptographic_material_providers.smithygenerated.aws_cryptography_materialproviders.smithy_to_dafny.aws_cryptography_materialproviders_KeyringReference( + native_input.keyring + ) + is not None + ) + ) + else (Option_None()) + ), + algorithmSuiteId=( + ( + Option_Some( + aws_cryptographic_material_providers.smithygenerated.aws_cryptography_materialproviders.smithy_to_dafny.aws_cryptography_materialproviders_ESDKAlgorithmSuiteId( + native_input.algorithm_suite_id + ) + ) + ) + if (native_input.algorithm_suite_id is not None) + else (Option_None()) + ), + frameLength=( + (Option_Some(native_input.frame_length)) + if (native_input.frame_length is not None) + else (Option_None()) + ), + ) + + +def aws_cryptography_encryptionsdk_DecryptInput(native_input): + return DafnyDecryptInput( + ciphertext=Seq(native_input.ciphertext), + materialsManager=( + ( + Option_Some( + aws_cryptographic_material_providers.smithygenerated.aws_cryptography_materialproviders.smithy_to_dafny.aws_cryptography_materialproviders_CryptographicMaterialsManagerReference( + native_input.materials_manager + ) + ) + ) + if ( + (native_input.materials_manager is not None) + and ( + aws_cryptographic_material_providers.smithygenerated.aws_cryptography_materialproviders.smithy_to_dafny.aws_cryptography_materialproviders_CryptographicMaterialsManagerReference( + native_input.materials_manager + ) + is not None + ) + ) + else (Option_None()) + ), + keyring=( + ( + Option_Some( + aws_cryptographic_material_providers.smithygenerated.aws_cryptography_materialproviders.smithy_to_dafny.aws_cryptography_materialproviders_KeyringReference( + native_input.keyring + ) + ) + ) + if ( + (native_input.keyring is not None) + and ( + aws_cryptographic_material_providers.smithygenerated.aws_cryptography_materialproviders.smithy_to_dafny.aws_cryptography_materialproviders_KeyringReference( + native_input.keyring + ) + is not None + ) + ) + else (Option_None()) + ), + encryptionContext=( + ( + Option_Some( + Map( + { + Seq(key.encode("utf-8")): Seq(value.encode("utf-8")) + for (key, value) in native_input.encryption_context.items() + } + ) + ) + ) + if (native_input.encryption_context is not None) + else (Option_None()) + ), + ) + + +def aws_cryptography_encryptionsdk_EncryptOutput(native_input): + return DafnyEncryptOutput( + ciphertext=Seq(native_input.ciphertext), + encryptionContext=Map( + { + Seq(key.encode("utf-8")): Seq(value.encode("utf-8")) + for (key, value) in native_input.encryption_context.items() + } + ), + algorithmSuiteId=aws_cryptographic_material_providers.smithygenerated.aws_cryptography_materialproviders.smithy_to_dafny.aws_cryptography_materialproviders_ESDKAlgorithmSuiteId( + native_input.algorithm_suite_id + ), + ) + + +def aws_cryptography_encryptionsdk_DecryptOutput(native_input): + return DafnyDecryptOutput( + plaintext=Seq(native_input.plaintext), + encryptionContext=Map( + { + Seq(key.encode("utf-8")): Seq(value.encode("utf-8")) + for (key, value) in native_input.encryption_context.items() + } + ), + algorithmSuiteId=aws_cryptographic_material_providers.smithygenerated.aws_cryptography_materialproviders.smithy_to_dafny.aws_cryptography_materialproviders_ESDKAlgorithmSuiteId( + native_input.algorithm_suite_id + ), + ) + + +def aws_cryptography_encryptionsdk_AtomicPrimitivesReference(native_input): + return native_input._config.dafnyImplInterface.impl + + +def aws_cryptography_encryptionsdk_NetV4_0_0_RetryPolicy(native_input): + if native_input == "FORBID_RETRY": + return NetV4__0__0__RetryPolicy_FORBID__RETRY() + + elif native_input == "ALLOW_RETRY": + return NetV4__0__0__RetryPolicy_ALLOW__RETRY() + + else: + raise ValueError(f"No recognized enum value in enum type: {native_input=}") + + +def aws_cryptography_encryptionsdk_AwsEncryptionSdkConfig(native_input): + return DafnyAwsEncryptionSdkConfig( + commitmentPolicy=( + ( + Option_Some( + aws_cryptographic_material_providers.smithygenerated.aws_cryptography_materialproviders.smithy_to_dafny.aws_cryptography_materialproviders_ESDKCommitmentPolicy( + native_input.commitment_policy + ) + ) + ) + if (native_input.commitment_policy is not None) + else (Option_None()) + ), + maxEncryptedDataKeys=( + (Option_Some(native_input.max_encrypted_data_keys)) + if (native_input.max_encrypted_data_keys is not None) + else (Option_None()) + ), + netV4__0__0__RetryPolicy=( + ( + Option_Some( + aws_encryption_sdk_dafny.smithygenerated.aws_cryptography_encryptionsdk.smithy_to_dafny.aws_cryptography_encryptionsdk_NetV4_0_0_RetryPolicy( + native_input.net_v4_0_0_retry_policy + ) + ) + ) + if (native_input.net_v4_0_0_retry_policy is not None) + else (Option_None()) + ), + ) + + +def aws_cryptography_encryptionsdk_MaterialProvidersReference(native_input): + return native_input._config.dafnyImplInterface.impl diff --git a/AwsEncryptionSDK/runtimes/python/test/internaldafny/__init__.py b/AwsEncryptionSDK/runtimes/python/test/internaldafny/__init__.py new file mode 100644 index 000000000..f94fd12a2 --- /dev/null +++ b/AwsEncryptionSDK/runtimes/python/test/internaldafny/__init__.py @@ -0,0 +1,2 @@ +# Copyright Amazon.com Inc. or its affiliates. All Rights Reserved. +# SPDX-License-Identifier: Apache-2.0 diff --git a/AwsEncryptionSDK/runtimes/python/test/internaldafny/generated/dafny_test-py.dtr b/AwsEncryptionSDK/runtimes/python/test/internaldafny/generated/dafny_test-py.dtr new file mode 100644 index 000000000..335d575ab --- /dev/null +++ b/AwsEncryptionSDK/runtimes/python/test/internaldafny/generated/dafny_test-py.dtr @@ -0,0 +1,12 @@ +file_format_version = "1.0" +dafny_version = "4.9.0.0" +[options_by_module.Fixtures] +legacy-module-names = false +[options_by_module.TestRequiredEncryptionContext] +legacy-module-names = false +[options_by_module.TestReproducedEncryptionContext] +legacy-module-names = false +[options_by_module.TestEncryptDecrypt] +legacy-module-names = false +[options_by_module.TestCreateEsdkClient] +legacy-module-names = false diff --git a/AwsEncryptionSDK/runtimes/python/test/internaldafny/test_dafny_wrapper.py b/AwsEncryptionSDK/runtimes/python/test/internaldafny/test_dafny_wrapper.py new file mode 100644 index 000000000..e617c3e2e --- /dev/null +++ b/AwsEncryptionSDK/runtimes/python/test/internaldafny/test_dafny_wrapper.py @@ -0,0 +1,21 @@ +# Copyright Amazon.com Inc. or its affiliates. All Rights Reserved. +# SPDX-License-Identifier: Apache-2.0 + +""" +Wrapper file for executing Dafny tests from pytest. +This allows us to import modules required by Dafny-generated tests +before executing Dafny-generated tests. +pytest will find and execute the `test_dafny` method below, +which will execute the `internaldafny_test_executor.py` file in the `dafny` directory. +""" + +import sys + +internaldafny_dir = '/'.join(__file__.split("/")[:-1]) + +sys.path.append(internaldafny_dir + "/extern") +sys.path.append(internaldafny_dir + "/generated") + + +def test_dafny(): + from .generated import __main__ diff --git a/AwsEncryptionSDK/runtimes/python/tox.ini b/AwsEncryptionSDK/runtimes/python/tox.ini new file mode 100644 index 000000000..971b68b0e --- /dev/null +++ b/AwsEncryptionSDK/runtimes/python/tox.ini @@ -0,0 +1,14 @@ +[tox] +isolated_build = True +envlist = + py{311,312} + +[testenv] +skip_install = true +allowlist_externals = poetry +passenv = AWS_* +commands_pre = + poetry lock + poetry install +commands = + poetry run pytest -s -v test/ diff --git a/TestVectors/Makefile b/TestVectors/Makefile index 21c6dcf9e..2c7169d19 100644 --- a/TestVectors/Makefile +++ b/TestVectors/Makefile @@ -194,6 +194,11 @@ test_generate_vectors_go: go -C runtimes/go/ImplementationFromDafny-go run ImplementationFromDafny.go encrypt-manifest --encrypt-manifest-output ../ cp dafny/TestVectors/test/keys.json runtimes/go +test_generate_vectors_python: + rm -rf runtimes/python/.tox + python3 -m tox -c runtimes/python --verbose -e cli -- encrypt-manifest --encrypt-manifest-output runtimes/python + cp dafny/TestVectors/test/keys.json runtimes/python + test_encrypt_vectors_java: gradle -p runtimes/java run --args="encrypt --manifest-path . --decrypt-manifest-path ." @@ -211,6 +216,10 @@ test_encrypt_vectors_rust: test_encrypt_vectors_go: go -C runtimes/go/ImplementationFromDafny-go run ImplementationFromDafny.go encrypt --manifest-path=.. --decrypt-manifest-path=.. +test_encrypt_vectors_python: + rm -rf runtimes/python/.tox + python3 -m tox -c runtimes/python --verbose -e cli -- encrypt --manifest-path runtimes/python --decrypt-manifest-path runtimes/python + test_decrypt_encrypt_vectors_java: gradle -p runtimes/java run --args="decrypt --manifest-path . --manifest-name decrypt-manifest.json" @@ -234,6 +243,10 @@ test_decrypt_encrypt_vectors_rust: test_decrypt_encrypt_vectors_go: go -C runtimes/go/ImplementationFromDafny-go run ImplementationFromDafny.go decrypt --manifest-path=.. --manifest-name=decrypt-manifest.json +test_decrypt_encrypt_vectors_python: + rm -rf runtimes/python/.tox + python3 -m tox -c runtimes/python --verbose -e cli -- decrypt --manifest-path runtimes/python --manifest-name decrypt-manifest.json + _polymorph_dependencies: @echo "No polymorphing of dependency" @@ -248,3 +261,24 @@ _sed_types_file_add_extern: _sed_index_file_add_extern: @echo "No extern to process for ESDK TestVectors" + +PYTHON_MODULE_NAME=aws_encryption_sdk_test_vectors + +TRANSLATION_RECORD_PYTHON := \ + --translation-record ../mpl/StandardLibrary/runtimes/python/src/smithy_dafny_standard_library/internaldafny/generated/dafny_src-py.dtr \ + --translation-record ../mpl/ComAmazonawsKms/runtimes/python/src/aws_cryptography_internal_kms/internaldafny/generated/dafny_src-py.dtr \ + --translation-record ../mpl/ComAmazonawsDynamodb/runtimes/python/src/aws_cryptography_internal_dynamodb/internaldafny/generated/dafny_src-py.dtr \ + --translation-record ../mpl/AwsCryptographyPrimitives/runtimes/python/src/aws_cryptography_primitives/internaldafny/generated/dafny_src-py.dtr \ + --translation-record ../mpl/AwsCryptographicMaterialProviders/runtimes/python/src/aws_cryptographic_material_providers/internaldafny/generated/dafny_src-py.dtr \ + --translation-record ../mpl/TestVectorsAwsCryptographicMaterialProviders/runtimes/python/src/aws_cryptography_materialproviders_test_vectors/internaldafny/generated/dafny_src-py.dtr \ + --translation-record ../AwsEncryptionSDK/runtimes/python/src/aws_encryption_sdk_dafny/internaldafny/generated/dafny_src-py.dtr + +PYTHON_DEPENDENCY_MODULE_NAMES := \ + --dependency-library-name=aws.cryptography.primitives=aws_cryptography_primitives \ + --dependency-library-name=com.amazonaws.kms=aws_cryptography_internal_kms \ + --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=smithy.api=aws_cryptographic_material_providers \ + --dependency-library-name=aws.cryptography.materialProvidersTestVectorKeys=aws_cryptographic_material_providers_test_vectors \ + --dependency-library-name=aws.cryptography.encryptionSdk=aws_encryption_sdk_dafny diff --git a/TestVectors/runtimes/python/.gitignore b/TestVectors/runtimes/python/.gitignore new file mode 100644 index 000000000..9cb72dcab --- /dev/null +++ b/TestVectors/runtimes/python/.gitignore @@ -0,0 +1,16 @@ +# Python build artifacts +__pycache__ +**/__pycache__ +*.pyc +src/**.egg-info/ +build +poetry.lock +**/poetry.lock +dist + +# Dafny-generated Python +**/internaldafny/generated/*.py + +# Python test artifacts +.tox +.pytest_cache diff --git a/TestVectors/runtimes/python/pyproject.toml b/TestVectors/runtimes/python/pyproject.toml new file mode 100644 index 000000000..7867d9ea3 --- /dev/null +++ b/TestVectors/runtimes/python/pyproject.toml @@ -0,0 +1,29 @@ +[tool.poetry] +name = "aws-encryption-sdk-test-vectors" +version = "0.1.0" +description = "" +authors = ["AWS Crypto Tools "] +packages = [ + { include = "aws_encryption_sdk_test_vectors", from = "src" } +] +# Include generated internaldafny files in package distributions, +# even though they are not included in version control +include = ["**/internaldafny/generated/*.py"] + +[tool.poetry.dependencies] +python = "^3.11.0" +aws-cryptographic-material-providers = { path = "../../../mpl/AwsCryptographicMaterialProviders/runtimes/python", develop = false} +aws-cryptography-internal-mpl-testvectors = { path = "../../../mpl/TestVectorsAwsCryptographicMaterialProviders/runtimes/python", develop = false} + +# Use the Dafny ESDK Python for type conversions to/from Dafny TestVectors code +aws-encryption-sdk-dafny = { path = "../../../AwsEncryptionSDK/runtimes/python", develop = false} + +# Run TestVectors against the released native ESDK-Python +aws-encryption-sdk = "4.0.0" + +[tool.poetry.group.test.dependencies] +pytest = "^7.4.0" + +[build-system] +requires = ["poetry-core<2.0.0"] +build-backend = "poetry.core.masonry.api" diff --git a/TestVectors/runtimes/python/src/aws_encryption_sdk_test_vectors/__init__.py b/TestVectors/runtimes/python/src/aws_encryption_sdk_test_vectors/__init__.py new file mode 100644 index 000000000..b9427e19d --- /dev/null +++ b/TestVectors/runtimes/python/src/aws_encryption_sdk_test_vectors/__init__.py @@ -0,0 +1,8 @@ +# Copyright Amazon.com Inc. or its affiliates. All Rights Reserved. +# SPDX-License-Identifier: Apache-2.0 + +# Initialize generated Dafny +from .internaldafny.generated import module_ + +# Initialize externs +from .internaldafny import extern diff --git a/TestVectors/runtimes/python/src/aws_encryption_sdk_test_vectors/internaldafny/extern/__init__.py b/TestVectors/runtimes/python/src/aws_encryption_sdk_test_vectors/internaldafny/extern/__init__.py new file mode 100644 index 000000000..c8c57bb1b --- /dev/null +++ b/TestVectors/runtimes/python/src/aws_encryption_sdk_test_vectors/internaldafny/extern/__init__.py @@ -0,0 +1,4 @@ +from . import ( + replace_dafny_main_method, + wrapped_esdk, +) diff --git a/TestVectors/runtimes/python/src/aws_encryption_sdk_test_vectors/internaldafny/extern/replace_dafny_main_method.py b/TestVectors/runtimes/python/src/aws_encryption_sdk_test_vectors/internaldafny/extern/replace_dafny_main_method.py new file mode 100644 index 000000000..c17188b4e --- /dev/null +++ b/TestVectors/runtimes/python/src/aws_encryption_sdk_test_vectors/internaldafny/extern/replace_dafny_main_method.py @@ -0,0 +1,16 @@ +# Copyright Amazon.com Inc. or its affiliates. All Rights Reserved. +# SPDX-License-Identifier: Apache-2.0 + +# ESDK TestVectors have 2 main methods; one in ESDK TestVectors, another in MPL TestVectors. +# This isn't really supported, and results in running the MPL TestVectors' main method. +# Other languages use sed on Dafny-generated code to replace the generated call to the main method. +# It's (arguably) less hacky to override the function that is called in Python. +import aws_encryption_sdk_test_vectors.internaldafny.generated.module_ as module_ +import aws_encryption_sdk_test_vectors.internaldafny.generated.WrappedESDKMain as WrappedESDKMain + + +def new_test_main(args): + WrappedESDKMain.default__.Main2(args) + + +module_.default__.Test____Main____ = new_test_main diff --git a/TestVectors/runtimes/python/src/aws_encryption_sdk_test_vectors/internaldafny/extern/wrapped_esdk.py b/TestVectors/runtimes/python/src/aws_encryption_sdk_test_vectors/internaldafny/extern/wrapped_esdk.py new file mode 100644 index 000000000..531f63956 --- /dev/null +++ b/TestVectors/runtimes/python/src/aws_encryption_sdk_test_vectors/internaldafny/extern/wrapped_esdk.py @@ -0,0 +1,178 @@ +# Copyright Amazon.com Inc. or its affiliates. All Rights Reserved. +# SPDX-License-Identifier: Apache-2.0 +import aws_encryption_sdk.streaming_client +import aws_encryption_sdk_test_vectors.internaldafny.generated.WrappedESDK as WrappedESDK +import smithy_dafny_standard_library.internaldafny.generated.Wrappers as Wrappers +import aws_encryption_sdk_dafny.smithygenerated.aws_cryptography_encryptionsdk.client +import aws_encryption_sdk_dafny.smithygenerated.aws_cryptography_encryptionsdk.config +import aws_encryption_sdk_dafny.internaldafny.generated.ESDK as ESDK +import aws_encryption_sdk_test_vectors.smithygenerated.aws_cryptography_encryptionsdk.shim as shim +from aws_encryption_sdk_dafny.smithygenerated.aws_cryptography_encryptionsdk.config import ( + dafny_config_to_smithy_config, +) +import aws_encryption_sdk +from aws_encryption_sdk.identifiers import CommitmentPolicy +from aws_encryption_sdk_dafny.smithygenerated.aws_cryptography_encryptionsdk.models import ( + EncryptInput, + EncryptOutput, + DecryptOutput, + DecryptInput, + NetV4_0_0_RetryPolicy, +) +from aws_encryption_sdk_dafny.smithygenerated.aws_cryptography_encryptionsdk.dafny_to_smithy import ( + aws_cryptography_encryptionsdk_EncryptInput as dafny_to_smithy_EncryptInput, + aws_cryptography_encryptionsdk_DecryptInput as dafny_to_smithy_DecryptInput, +) +from aws_encryption_sdk_dafny.smithygenerated.aws_cryptography_encryptionsdk.smithy_to_dafny import ( + aws_cryptography_encryptionsdk_DecryptOutput as smithy_to_dafny_DecryptOutput, + aws_cryptography_encryptionsdk_EncryptOutput as smithy_to_dafny_EncryptOutput, +) +from aws_encryption_sdk_dafny.smithygenerated.aws_cryptography_encryptionsdk.errors import ( + _smithy_error_to_dafny_error, +) +from aws_encryption_sdk.materials_managers.mpl.cmm import CryptoMaterialsManagerFromMPL +from aws_encryption_sdk.materials_managers.mpl.materials import ( + _mpl_algorithm_id_to_native_algorithm_id, +) +from aws_encryption_sdk.identifiers import AlgorithmSuite + + +def _esdk_dafny_commitment_policy_to_native(dafny_commitment_policy): + if dafny_commitment_policy == "FORBID_ENCRYPT_ALLOW_DECRYPT": + return CommitmentPolicy.FORBID_ENCRYPT_ALLOW_DECRYPT + elif dafny_commitment_policy == "REQUIRE_ENCRYPT_ALLOW_DECRYPT": + return CommitmentPolicy.REQUIRE_ENCRYPT_ALLOW_DECRYPT + elif dafny_commitment_policy == "REQUIRE_ENCRYPT_REQUIRE_DECRYPT": + return CommitmentPolicy.REQUIRE_ENCRYPT_REQUIRE_DECRYPT + else: + raise ValueError(f"Unsupported CommitmentPolicy: {dafny_commitment_policy}") + + +class DafnyESDKToNativeESDKShim: + + def __init__(self, native_esdk): + self.native_esdk = native_esdk + + def Encrypt(self, dafny_encrypt_input): + try: + native_encrypt_input = dafny_to_smithy_EncryptInput(dafny_encrypt_input) + + # Manual conversion of ESDK-Dafny EncryptInput to unmodelled native ESDK-Python encrypt parameters + native_esdk_input = { + "source": native_encrypt_input.plaintext, + "encryption_context": native_encrypt_input.encryption_context, + } + + if native_encrypt_input.keyring is not None: + native_esdk_input["keyring"] = native_encrypt_input.keyring + if native_encrypt_input.materials_manager is not None: + native_esdk_input["materials_manager"] = ( + native_encrypt_input.materials_manager + ) + if native_encrypt_input.algorithm_suite_id is not None: + native_esdk_input["algorithm"] = AlgorithmSuite.get_by_id( + _mpl_algorithm_id_to_native_algorithm_id( + native_encrypt_input.algorithm_suite_id + ) + ) + + native_esdk_ciphertext, native_esdk_header = self.native_esdk.encrypt( + **native_esdk_input + ) + + dafny_esdk_native_encrypt_output = EncryptOutput( + ciphertext=native_esdk_ciphertext, + encryption_context=native_esdk_header.encryption_context, + algorithm_suite_id=CryptoMaterialsManagerFromMPL._native_algorithm_id_to_mpl_algorithm_id( + native_esdk_header.algorithm.algorithm_id + ).value, + ) + + dafny_esdk_dafny_encrypt_output = smithy_to_dafny_EncryptOutput( + dafny_esdk_native_encrypt_output + ) + + return Wrappers.Result_Success(dafny_esdk_dafny_encrypt_output) + except Exception as e: + return Wrappers.Result_Failure(_smithy_error_to_dafny_error(e)) + + def Decrypt(self, dafny_decrypt_input): + + try: + + native_decrypt_input = dafny_to_smithy_DecryptInput(dafny_decrypt_input) + + # Manual conversion of ESDK-Dafny DecryptInput to unmodelled native ESDK-Python decrypt parameters + native_esdk_input = { + "source": native_decrypt_input.ciphertext, + "encryption_context": native_decrypt_input.encryption_context, + } + if native_decrypt_input.keyring is not None: + native_esdk_input["keyring"] = native_decrypt_input.keyring + if native_decrypt_input.materials_manager is not None: + native_esdk_input["materials_manager"] = ( + native_decrypt_input.materials_manager + ) + + native_esdk_plaintext, native_esdk_header = self.native_esdk.decrypt( + **native_esdk_input + ) + + dafny_esdk_native_decrypt_output = DecryptOutput( + plaintext=native_esdk_plaintext, + encryption_context=native_esdk_header.encryption_context, + algorithm_suite_id=CryptoMaterialsManagerFromMPL._native_algorithm_id_to_mpl_algorithm_id( + native_esdk_header.algorithm.algorithm_id + ).value, + ) + + dafny_esdk_dafny_decrypt_output = smithy_to_dafny_DecryptOutput( + dafny_esdk_native_decrypt_output + ) + + return Wrappers.Result_Success(dafny_esdk_dafny_decrypt_output) + except Exception as e: + return Wrappers.Result_Failure(_smithy_error_to_dafny_error(e)) + + +class default__(WrappedESDK.default__): + + # This commented-out method wraps the Dafny-generated ESDK. + # Not testing right now. + # @staticmethod + # def WrappedESDK(config): + # smithy_client = aws_encryption_sdk.smithygenerated.aws_cryptography_encryptionsdk.client.AwsEncryptionSdk( + # dafny_client=ESDK.default__.ESDK(config).value + # ) + # wrapped_client = shim.ESDKShim(smithy_client) + # return Wrappers.Result_Success(wrapped_client) + + @staticmethod + # Wrapper for the native ESDK-Python. + def WrappedESDK(dafny_config): + native_config = dafny_config_to_smithy_config(dafny_config) + + if native_config.net_v4_0_0_retry_policy == NetV4_0_0_RetryPolicy.ALLOW_RETRY: + raise ValueError("net 4.0.0 retry policy is not supported") + + commitment_policy = _esdk_dafny_commitment_policy_to_native( + native_config.commitment_policy + ) + + max_edks = ( + 1 + if native_config.max_encrypted_data_keys == 0 + else native_config.max_encrypted_data_keys + ) + + native_esdk = aws_encryption_sdk.EncryptionSDKClient( + commitment_policy=commitment_policy, + max_encrypted_data_keys=max_edks, + ) + + dafny_wrapped_esdk = DafnyESDKToNativeESDKShim(native_esdk) + + return Wrappers.Result_Success(dafny_wrapped_esdk) + + +WrappedESDK.default__ = default__ diff --git a/TestVectors/runtimes/python/src/aws_encryption_sdk_test_vectors/internaldafny/generated/dafny_src-py.dtr b/TestVectors/runtimes/python/src/aws_encryption_sdk_test_vectors/internaldafny/generated/dafny_src-py.dtr new file mode 100644 index 000000000..2e95eed63 --- /dev/null +++ b/TestVectors/runtimes/python/src/aws_encryption_sdk_test_vectors/internaldafny/generated/dafny_src-py.dtr @@ -0,0 +1,35 @@ +file_format_version = "1.0" +dafny_version = "4.9.0.0" +[options_by_module.WrappedAbstractAwsCryptographyEncryptionSdkService] +legacy-module-names = false +python-module-name = "aws_encryption_sdk_test_vectors.internaldafny.generated" +[options_by_module.WrappedESDK] +legacy-module-names = false +python-module-name = "aws_encryption_sdk_test_vectors.internaldafny.generated" +[options_by_module.EsdkManifestOptions] +legacy-module-names = false +python-module-name = "aws_encryption_sdk_test_vectors.internaldafny.generated" +[options_by_module.EsdkTestVectors] +legacy-module-names = false +python-module-name = "aws_encryption_sdk_test_vectors.internaldafny.generated" +[options_by_module.AllEsdkV4NoReqEc] +legacy-module-names = false +python-module-name = "aws_encryption_sdk_test_vectors.internaldafny.generated" +[options_by_module.AllEsdkV4WithReqEc] +legacy-module-names = false +python-module-name = "aws_encryption_sdk_test_vectors.internaldafny.generated" +[options_by_module.WriteEsdkJsonManifests] +legacy-module-names = false +python-module-name = "aws_encryption_sdk_test_vectors.internaldafny.generated" +[options_by_module.WriteVectors] +legacy-module-names = false +python-module-name = "aws_encryption_sdk_test_vectors.internaldafny.generated" +[options_by_module.ParseEsdkJsonManifest] +legacy-module-names = false +python-module-name = "aws_encryption_sdk_test_vectors.internaldafny.generated" +[options_by_module.EsdkTestManifests] +legacy-module-names = false +python-module-name = "aws_encryption_sdk_test_vectors.internaldafny.generated" +[options_by_module.WrappedESDKMain] +legacy-module-names = false +python-module-name = "aws_encryption_sdk_test_vectors.internaldafny.generated" diff --git a/TestVectors/runtimes/python/src/aws_encryption_sdk_test_vectors/smithygenerated/aws_cryptography_encryptionsdk/__init__.py b/TestVectors/runtimes/python/src/aws_encryption_sdk_test_vectors/smithygenerated/aws_cryptography_encryptionsdk/__init__.py new file mode 100644 index 000000000..09be6133b --- /dev/null +++ b/TestVectors/runtimes/python/src/aws_encryption_sdk_test_vectors/smithygenerated/aws_cryptography_encryptionsdk/__init__.py @@ -0,0 +1,3 @@ +# Copyright Amazon.com Inc. or its affiliates. All Rights Reserved. +# SPDX-License-Identifier: Apache-2.0 +# Do not modify this file. This file is machine generated, and any changes to it will be overwritten. diff --git a/TestVectors/runtimes/python/src/aws_encryption_sdk_test_vectors/smithygenerated/aws_cryptography_encryptionsdk/shim.py b/TestVectors/runtimes/python/src/aws_encryption_sdk_test_vectors/smithygenerated/aws_cryptography_encryptionsdk/shim.py new file mode 100644 index 000000000..75c1c62f1 --- /dev/null +++ b/TestVectors/runtimes/python/src/aws_encryption_sdk_test_vectors/smithygenerated/aws_cryptography_encryptionsdk/shim.py @@ -0,0 +1,66 @@ +# Copyright Amazon.com Inc. or its affiliates. All Rights Reserved. +# SPDX-License-Identifier: Apache-2.0 +# Do not modify this file. This file is machine generated, and any changes to it will be overwritten. + +from aws_encryption_sdk_dafny.internaldafny.generated.AwsCryptographyEncryptionSdkTypes import ( + DecryptInput_DecryptInput as DafnyDecryptInput, + DecryptOutput_DecryptOutput as DafnyDecryptOutput, + EncryptInput_EncryptInput as DafnyEncryptInput, + EncryptOutput_EncryptOutput as DafnyEncryptOutput, +) +import aws_encryption_sdk_dafny.internaldafny.generated.module_ +import aws_encryption_sdk_dafny.smithygenerated.aws_cryptography_encryptionsdk.dafny_to_smithy +import aws_encryption_sdk_dafny.smithygenerated.aws_cryptography_encryptionsdk.errors +from aws_encryption_sdk_dafny.smithygenerated.aws_cryptography_encryptionsdk.errors import ( + CollectionOfErrors, + OpaqueError, + ServiceError, + _smithy_error_to_dafny_error, +) +import aws_encryption_sdk_dafny.smithygenerated.aws_cryptography_encryptionsdk.models +import aws_encryption_sdk_dafny.smithygenerated.aws_cryptography_encryptionsdk.smithy_to_dafny +from typing import Any + + +import smithy_dafny_standard_library.internaldafny.generated.Wrappers as Wrappers +import aws_encryption_sdk_dafny.internaldafny.generated.AwsCryptographyEncryptionSdkTypes +import aws_encryption_sdk_dafny.smithygenerated.aws_cryptography_encryptionsdk.client as client_impl + + +class ESDKShim( + aws_encryption_sdk_dafny.internaldafny.generated.AwsCryptographyEncryptionSdkTypes.IAwsEncryptionSdkClient +): + def __init__(self, _impl: client_impl): + self._impl = _impl + + def Encrypt(self, input): + try: + smithy_client_request: ( + aws_encryption_sdk_dafny.smithygenerated.aws_cryptography_encryptionsdk.models.EncryptInput + ) = aws_encryption_sdk_dafny.smithygenerated.aws_cryptography_encryptionsdk.dafny_to_smithy.aws_cryptography_encryptionsdk_EncryptInput( + input + ) + smithy_client_response = self._impl.encrypt(smithy_client_request) + return Wrappers.Result_Success( + aws_encryption_sdk_dafny.smithygenerated.aws_cryptography_encryptionsdk.smithy_to_dafny.aws_cryptography_encryptionsdk_EncryptOutput( + smithy_client_response + ) + ) + except Exception as e: + return Wrappers.Result_Failure(_smithy_error_to_dafny_error(e)) + + def Decrypt(self, input): + try: + smithy_client_request: ( + aws_encryption_sdk_dafny.smithygenerated.aws_cryptography_encryptionsdk.models.DecryptInput + ) = aws_encryption_sdk_dafny.smithygenerated.aws_cryptography_encryptionsdk.dafny_to_smithy.aws_cryptography_encryptionsdk_DecryptInput( + input + ) + smithy_client_response = self._impl.decrypt(smithy_client_request) + return Wrappers.Result_Success( + aws_encryption_sdk_dafny.smithygenerated.aws_cryptography_encryptionsdk.smithy_to_dafny.aws_cryptography_encryptionsdk_DecryptOutput( + smithy_client_response + ) + ) + except Exception as e: + return Wrappers.Result_Failure(_smithy_error_to_dafny_error(e)) diff --git a/TestVectors/runtimes/python/test/internaldafny/__init__.py b/TestVectors/runtimes/python/test/internaldafny/__init__.py new file mode 100644 index 000000000..f94fd12a2 --- /dev/null +++ b/TestVectors/runtimes/python/test/internaldafny/__init__.py @@ -0,0 +1,2 @@ +# Copyright Amazon.com Inc. or its affiliates. All Rights Reserved. +# SPDX-License-Identifier: Apache-2.0 diff --git a/TestVectors/runtimes/python/test/internaldafny/extern/TestWrappedESDKMain_extern.py b/TestVectors/runtimes/python/test/internaldafny/extern/TestWrappedESDKMain_extern.py new file mode 100644 index 000000000..574e31c52 --- /dev/null +++ b/TestVectors/runtimes/python/test/internaldafny/extern/TestWrappedESDKMain_extern.py @@ -0,0 +1,10 @@ +import TestWrappedESDKMain +import _dafny +import os + +class default__(TestWrappedESDKMain.default__): + @staticmethod + def GetTestVectorExecutionDirectory(): + return _dafny.Seq(os.getcwd() + "/../../") + +TestWrappedESDKMain.default__ = default__ \ No newline at end of file diff --git a/TestVectors/runtimes/python/test/internaldafny/extern/__init__.py b/TestVectors/runtimes/python/test/internaldafny/extern/__init__.py new file mode 100644 index 000000000..0e8ddce01 --- /dev/null +++ b/TestVectors/runtimes/python/test/internaldafny/extern/__init__.py @@ -0,0 +1,3 @@ +from . import ( + TestWrappedESDKMain_extern, +) \ No newline at end of file diff --git a/TestVectors/runtimes/python/test/internaldafny/generated/dafny_test-py.dtr b/TestVectors/runtimes/python/test/internaldafny/generated/dafny_test-py.dtr new file mode 100644 index 000000000..ede2d6ffa --- /dev/null +++ b/TestVectors/runtimes/python/test/internaldafny/generated/dafny_test-py.dtr @@ -0,0 +1,4 @@ +file_format_version = "1.0" +dafny_version = "4.9.0.0" +[options_by_module.TestWrappedESDKMain] +legacy-module-names = false diff --git a/TestVectors/runtimes/python/test/internaldafny/test_dafny_wrapper.py b/TestVectors/runtimes/python/test/internaldafny/test_dafny_wrapper.py new file mode 100644 index 000000000..2a70bb22c --- /dev/null +++ b/TestVectors/runtimes/python/test/internaldafny/test_dafny_wrapper.py @@ -0,0 +1,22 @@ +# Copyright Amazon.com Inc. or its affiliates. All Rights Reserved. +# SPDX-License-Identifier: Apache-2.0 + +""" +Wrapper file for executing Dafny tests from pytest. +This allows us to import modules required by Dafny-generated tests +before executing Dafny-generated tests. +pytest will find and execute the `test_dafny` method below, +which will execute the `internaldafny_test_executor.py` file in the `dafny` directory. +""" + +import sys + +internaldafny_dir = '/'.join(__file__.split("/")[:-1]) + +sys.path.append(internaldafny_dir + "/extern") +sys.path.append(internaldafny_dir + "/generated") + +from . import extern + +def test_dafny(): + from .generated import __main__ diff --git a/TestVectors/runtimes/python/tox.ini b/TestVectors/runtimes/python/tox.ini new file mode 100644 index 000000000..fdd406a52 --- /dev/null +++ b/TestVectors/runtimes/python/tox.ini @@ -0,0 +1,26 @@ +[tox] +isolated_build = True +envlist = + py{311,312} + +[testenv] +skip_install = true +allowlist_externals = poetry +passenv = AWS_* +commands_pre = + poetry lock + poetry install +commands = + poetry run pytest -s -v test/ + +[testenv:cli] +skip_install = true +allowlist_externals = poetry +passenv = AWS_* +setenv = VIRTUALENV_DOWNLOAD=0 + PIP_DISABLE_PIP_VERSION_CHECK=1 +commands_pre = + poetry lock + poetry install --with test +commands = + poetry run python src/aws_encryption_sdk_test_vectors/internaldafny/generated {posargs} \ No newline at end of file