m

aws · Dec 13, 2024 · 7975d15 · 7975d15
1 parent 76b9b11
commit 7975d15
Show file tree

Hide file tree

Showing 88 changed files with 10,048 additions and 0 deletions.
diff --git a/TestVectors/runtimes/python/poetry.lock b/TestVectors/runtimes/python/poetry.lock
diff --git a/TestVectors/runtimes/python/pyproject.toml b/TestVectors/runtimes/python/pyproject.toml
@@ -0,0 +1,24 @@
+[tool.poetry]
+name = "aws-encryption-sdk-test-vectors"
+version = "0.1.0"
+description = ""
+authors = ["AWS Crypto Tools <[email protected]>"]
+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}
+aws-encryption-sdk = { path = "../../../AwsEncryptionSDK/runtimes/python", develop = false}
+
+[tool.poetry.group.test.dependencies]
+pytest = "^7.4.0"
+
+[build-system]
+requires = ["poetry-core"]
+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
@@ -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/.../runtimes/python/src/aws_encryption_sdk_test_vectors/__pycache__/__init__.cpython-311.pyc b/.../runtimes/python/src/aws_encryption_sdk_test_vectors/__pycache__/__init__.cpython-311.pyc
diff --git a/.../runtimes/python/src/aws_encryption_sdk_test_vectors/__pycache__/__init__.cpython-312.pyc b/.../runtimes/python/src/aws_encryption_sdk_test_vectors/__pycache__/__init__.cpython-312.pyc
diff --git a/...tors/runtimes/python/src/aws_encryption_sdk_test_vectors/internaldafny/extern/__init__.py b/...tors/runtimes/python/src/aws_encryption_sdk_test_vectors/internaldafny/extern/__init__.py
@@ -0,0 +1,3 @@
+from . import (
+    wrapped_esdk,
+)
diff --git a/...aws_encryption_sdk_test_vectors/internaldafny/extern/__pycache__/__init__.cpython-311.pyc b/...aws_encryption_sdk_test_vectors/internaldafny/extern/__pycache__/__init__.cpython-311.pyc
diff --git a/...aws_encryption_sdk_test_vectors/internaldafny/extern/__pycache__/__init__.cpython-312.pyc b/...aws_encryption_sdk_test_vectors/internaldafny/extern/__pycache__/__init__.cpython-312.pyc
diff --git a/...encryption_sdk_test_vectors/internaldafny/extern/__pycache__/wrapped_esdk.cpython-311.pyc b/...encryption_sdk_test_vectors/internaldafny/extern/__pycache__/wrapped_esdk.cpython-311.pyc
diff --git a/...encryption_sdk_test_vectors/internaldafny/extern/__pycache__/wrapped_esdk.cpython-312.pyc b/...encryption_sdk_test_vectors/internaldafny/extern/__pycache__/wrapped_esdk.cpython-312.pyc
diff --git a/.../runtimes/python/src/aws_encryption_sdk_test_vectors/internaldafny/extern/wrapped_esdk.py b/.../runtimes/python/src/aws_encryption_sdk_test_vectors/internaldafny/extern/wrapped_esdk.py
@@ -0,0 +1,18 @@
+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.smithygenerated.aws_cryptography_encryptionsdk.client
+import aws_encryption_sdk.smithygenerated.aws_cryptography_encryptionsdk.config
+import aws_encryption_sdk.internaldafny.generated.EncryptionSdk as EncryptionSdk
+import aws_encryption_sdk_test_vectors.smithygenerated.aws_cryptography_encryptionsdk.shim as shim
+
+class default__(WrappedESDK.default__):
+
+  @staticmethod
+  def WrappedESDK(config):  
+    smithy_client = aws_encryption_sdk.smithygenerated.aws_cryptography_encryptionsdk.client.AwsEncryptionSdk(
+      dafny_client=EncryptionSdk.default__.ESDK(config).value
+    )
+    wrapped_client = shim.ESDKShim(smithy_client)
+    return Wrappers.Result_Success(wrapped_client)
+
+WrappedESDK.default__ = default__
diff --git a/...es/python/src/aws_encryption_sdk_test_vectors/internaldafny/generated/AllEsdkV4NoReqEc.py b/...es/python/src/aws_encryption_sdk_test_vectors/internaldafny/generated/AllEsdkV4NoReqEc.py
diff --git a/.../python/src/aws_encryption_sdk_test_vectors/internaldafny/generated/AllEsdkV4WithReqEc.py b/.../python/src/aws_encryption_sdk_test_vectors/internaldafny/generated/AllEsdkV4WithReqEc.py
diff --git a/...python/src/aws_encryption_sdk_test_vectors/internaldafny/generated/EsdkManifestOptions.py b/...python/src/aws_encryption_sdk_test_vectors/internaldafny/generated/EsdkManifestOptions.py
diff --git a/...s/python/src/aws_encryption_sdk_test_vectors/internaldafny/generated/EsdkTestManifests.py b/...s/python/src/aws_encryption_sdk_test_vectors/internaldafny/generated/EsdkTestManifests.py
diff --git a/...mes/python/src/aws_encryption_sdk_test_vectors/internaldafny/generated/EsdkTestVectors.py b/...mes/python/src/aws_encryption_sdk_test_vectors/internaldafny/generated/EsdkTestVectors.py
diff --git a/...thon/src/aws_encryption_sdk_test_vectors/internaldafny/generated/ParseEsdkJsonManifest.py b/...thon/src/aws_encryption_sdk_test_vectors/internaldafny/generated/ParseEsdkJsonManifest.py
diff --git a/...untimes/python/src/aws_encryption_sdk_test_vectors/internaldafny/generated/WrappedESDK.py b/...untimes/python/src/aws_encryption_sdk_test_vectors/internaldafny/generated/WrappedESDK.py
diff --git a/...mes/python/src/aws_encryption_sdk_test_vectors/internaldafny/generated/WrappedESDKMain.py b/...mes/python/src/aws_encryption_sdk_test_vectors/internaldafny/generated/WrappedESDKMain.py
diff --git a/...hon/src/aws_encryption_sdk_test_vectors/internaldafny/generated/WriteEsdkJsonManifests.py b/...hon/src/aws_encryption_sdk_test_vectors/internaldafny/generated/WriteEsdkJsonManifests.py
diff --git a/...ntimes/python/src/aws_encryption_sdk_test_vectors/internaldafny/generated/WriteVectors.py b/...ntimes/python/src/aws_encryption_sdk_test_vectors/internaldafny/generated/WriteVectors.py
diff --git a/...s/runtimes/python/src/aws_encryption_sdk_test_vectors/internaldafny/generated/__main__.py b/...s/runtimes/python/src/aws_encryption_sdk_test_vectors/internaldafny/generated/__main__.py
@@ -0,0 +1,15 @@
+# Dafny program the_program compiled into Python
+import sys
+from typing import Callable, Any, TypeVar, NamedTuple
+from math import floor
+from itertools import count
+
+import aws_encryption_sdk_test_vectors.internaldafny.generated.module_ as module_
+import _dafny as _dafny
+
+try:
+    dafnyArgs = [_dafny.Seq(a) for a in sys.argv]
+    module_.default__.Test____Main____(dafnyArgs)
+except _dafny.HaltException as e:
+    _dafny.print("[Program halted] " + e.message + "\n")
+    sys.exit(1)
diff --git a/...ion_sdk_test_vectors/internaldafny/generated/__pycache__/AllEsdkV4NoReqEc.cpython-311.pyc b/...ion_sdk_test_vectors/internaldafny/generated/__pycache__/AllEsdkV4NoReqEc.cpython-311.pyc
diff --git a/...ion_sdk_test_vectors/internaldafny/generated/__pycache__/AllEsdkV4NoReqEc.cpython-312.pyc b/...ion_sdk_test_vectors/internaldafny/generated/__pycache__/AllEsdkV4NoReqEc.cpython-312.pyc
diff --git a/...n_sdk_test_vectors/internaldafny/generated/__pycache__/AllEsdkV4WithReqEc.cpython-311.pyc b/...n_sdk_test_vectors/internaldafny/generated/__pycache__/AllEsdkV4WithReqEc.cpython-311.pyc
diff --git a/...n_sdk_test_vectors/internaldafny/generated/__pycache__/AllEsdkV4WithReqEc.cpython-312.pyc b/...n_sdk_test_vectors/internaldafny/generated/__pycache__/AllEsdkV4WithReqEc.cpython-312.pyc
diff --git a/..._sdk_test_vectors/internaldafny/generated/__pycache__/EsdkManifestOptions.cpython-311.pyc b/..._sdk_test_vectors/internaldafny/generated/__pycache__/EsdkManifestOptions.cpython-311.pyc
diff --git a/..._sdk_test_vectors/internaldafny/generated/__pycache__/EsdkManifestOptions.cpython-312.pyc b/..._sdk_test_vectors/internaldafny/generated/__pycache__/EsdkManifestOptions.cpython-312.pyc
diff --git a/...on_sdk_test_vectors/internaldafny/generated/__pycache__/EsdkTestManifests.cpython-311.pyc b/...on_sdk_test_vectors/internaldafny/generated/__pycache__/EsdkTestManifests.cpython-311.pyc
diff --git a/...on_sdk_test_vectors/internaldafny/generated/__pycache__/EsdkTestManifests.cpython-312.pyc b/...on_sdk_test_vectors/internaldafny/generated/__pycache__/EsdkTestManifests.cpython-312.pyc
diff --git a/...tion_sdk_test_vectors/internaldafny/generated/__pycache__/EsdkTestVectors.cpython-311.pyc b/...tion_sdk_test_vectors/internaldafny/generated/__pycache__/EsdkTestVectors.cpython-311.pyc
diff --git a/...tion_sdk_test_vectors/internaldafny/generated/__pycache__/EsdkTestVectors.cpython-312.pyc b/...tion_sdk_test_vectors/internaldafny/generated/__pycache__/EsdkTestVectors.cpython-312.pyc
diff --git a/...dk_test_vectors/internaldafny/generated/__pycache__/ParseEsdkJsonManifest.cpython-311.pyc b/...dk_test_vectors/internaldafny/generated/__pycache__/ParseEsdkJsonManifest.cpython-311.pyc
diff --git a/...dk_test_vectors/internaldafny/generated/__pycache__/ParseEsdkJsonManifest.cpython-312.pyc b/...dk_test_vectors/internaldafny/generated/__pycache__/ParseEsdkJsonManifest.cpython-312.pyc
diff --git a/...cryption_sdk_test_vectors/internaldafny/generated/__pycache__/WrappedESDK.cpython-311.pyc b/...cryption_sdk_test_vectors/internaldafny/generated/__pycache__/WrappedESDK.cpython-311.pyc
diff --git a/...cryption_sdk_test_vectors/internaldafny/generated/__pycache__/WrappedESDK.cpython-312.pyc b/...cryption_sdk_test_vectors/internaldafny/generated/__pycache__/WrappedESDK.cpython-312.pyc
diff --git a/...tion_sdk_test_vectors/internaldafny/generated/__pycache__/WrappedESDKMain.cpython-311.pyc b/...tion_sdk_test_vectors/internaldafny/generated/__pycache__/WrappedESDKMain.cpython-311.pyc
diff --git a/...tion_sdk_test_vectors/internaldafny/generated/__pycache__/WrappedESDKMain.cpython-312.pyc b/...tion_sdk_test_vectors/internaldafny/generated/__pycache__/WrappedESDKMain.cpython-312.pyc
diff --git a/...k_test_vectors/internaldafny/generated/__pycache__/WriteEsdkJsonManifests.cpython-311.pyc b/...k_test_vectors/internaldafny/generated/__pycache__/WriteEsdkJsonManifests.cpython-311.pyc
diff --git a/...k_test_vectors/internaldafny/generated/__pycache__/WriteEsdkJsonManifests.cpython-312.pyc b/...k_test_vectors/internaldafny/generated/__pycache__/WriteEsdkJsonManifests.cpython-312.pyc
diff --git a/...ryption_sdk_test_vectors/internaldafny/generated/__pycache__/WriteVectors.cpython-311.pyc b/...ryption_sdk_test_vectors/internaldafny/generated/__pycache__/WriteVectors.cpython-311.pyc
diff --git a/...ryption_sdk_test_vectors/internaldafny/generated/__pycache__/WriteVectors.cpython-312.pyc b/...ryption_sdk_test_vectors/internaldafny/generated/__pycache__/WriteVectors.cpython-312.pyc
diff --git a/...s_encryption_sdk_test_vectors/internaldafny/generated/__pycache__/module_.cpython-311.pyc b/...s_encryption_sdk_test_vectors/internaldafny/generated/__pycache__/module_.cpython-311.pyc
diff --git a/...s_encryption_sdk_test_vectors/internaldafny/generated/__pycache__/module_.cpython-312.pyc b/...s_encryption_sdk_test_vectors/internaldafny/generated/__pycache__/module_.cpython-312.pyc
diff --git a/...times/python/src/aws_encryption_sdk_test_vectors/internaldafny/generated/dafny_src-py.dtr b/...times/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"