Skip to content

Commit 9bbb645

Browse files
?
1 parent 39dd9e6 commit 9bbb645

File tree

5 files changed

+76
-47
lines changed

5 files changed

+76
-47
lines changed

DynamoDbEncryption/Makefile

Lines changed: 0 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -3,11 +3,8 @@
33

44
CORES=2
55

6-
<<<<<<< HEAD
76
ENABLE_EXTERN_PROCESSING=1
8-
=======
97
TRANSPILE_TESTS_IN_RUST=1
10-
>>>>>>> main
118

129
include ../SharedMakefile.mk
1310

@@ -103,12 +100,6 @@ SERVICE_DEPS_DynamoDbEncryptionTransforms := \
103100
DynamoDbEncryption/dafny/DynamoDbEncryption \
104101
DynamoDbEncryption/dafny/StructuredEncryption \
105102
DynamoDbEncryption/dafny/DynamoDbItemEncryptor
106-
<<<<<<< HEAD
107-
108-
polymorph:
109-
export DAFNY_VERSION=4.2
110-
npm i --no-save prettier@3 [email protected]
111-
make polymorph_code_gen PROJECT_DEPENDENCIES=
112103

113104
# Python
114105

@@ -195,5 +186,3 @@ _sed_index_file_add_extern:
195186
$(MAKE) _sed_file SED_FILE_PATH=$(ITEMENCRYPTOR_LEGACY_FILE_PATH) SED_BEFORE_STRING=$(ITEMENCRYPTOR_LEGACY_FILE_WITHOUT_EXTERN_STRING) SED_AFTER_STRING=$(ITEMENCRYPTOR_LEGACY_FILE_WITH_EXTERN_STRING)
196187
$(MAKE) _sed_file SED_FILE_PATH=$(TRANSFORMS_INDEX_FILE_PATH) SED_BEFORE_STRING=$(TRANSFORMS_INDEX_FILE_WITHOUT_EXTERN_STRING) SED_AFTER_STRING=$(TRANSFORMS_INDEX_FILE_WITH_EXTERN_STRING)
197188
$(MAKE) _sed_file SED_FILE_PATH=$(STRUCTUREDENCRYPTION_INDEX_FILE_PATH) SED_BEFORE_STRING=$(STRUCTUREDENCRYPTION_INDEX_FILE_WITHOUT_EXTERN_STRING) SED_AFTER_STRING=$(STRUCTUREDENCRYPTION_INDEX_FILE_WITH_EXTERN_STRING)
198-
=======
199-
>>>>>>> main

DynamoDbEncryption/runtimes/python/pyproject.toml

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -17,6 +17,6 @@ aws-cryptographic-material-providers = { path = "../../../submodules/MaterialPro
1717
[tool.poetry.group.test.dependencies]
1818
pytest = "^7.4.0"
1919

20-
# [build-system]
21-
# requires = ["poetry-core<2.0.0"]
22-
# build-backend = "poetry.core.masonry.api"
20+
[build-system]
21+
requires = ["poetry-core<2.0.0"]
22+
build-backend = "poetry.core.masonry.api"

TestVectors/Makefile

Lines changed: 42 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2,6 +2,7 @@
22
# SPDX-License-Identifier: Apache-2.0
33

44
CORES=2
5+
ENABLE_EXTERN_PROCESSING=1
56
TRANSPILE_TESTS_IN_RUST=1
67

78
include ../SharedMakefile.mk
@@ -64,6 +65,8 @@ PROJECT_INDEX := \
6465
submodules/MaterialProviders/TestVectorsAwsCryptographicMaterialProviders/dafny/KeyVectors/src/Index.dfy \
6566
DynamoDbEncryption/dafny/StructuredEncryption/src/Index.dfy \
6667
DynamoDbEncryption/dafny/DynamoDbEncryption/src/Index.dfy \
68+
DynamoDbEncryption/dafny/DynamoDbItemEncryptor/src/Index.dfy \
69+
DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/Index.dfy \
6770

6871
STD_LIBRARY=submodules/MaterialProviders/StandardLibrary
6972
SMITHY_DEPS=submodules/MaterialProviders/model
@@ -79,10 +82,49 @@ SERVICE_DEPS_DDBEncryption := \
7982
submodules/MaterialProviders/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore \
8083
DynamoDbEncryption/dafny/StructuredEncryption \
8184
DynamoDbEncryption/dafny/DynamoDbEncryption \
85+
DynamoDbEncryption/dafny/DynamoDbItemEncryptor \
86+
DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms \
8287
submodules/MaterialProviders/TestVectorsAwsCryptographicMaterialProviders/dafny/TestVectorsAwsCryptographicMaterialProviders \
8388

8489
transpile_implementation_rust: _remove_wrapped_client_rust
8590

8691
_remove_wrapped_client_rust:
8792
$(MAKE) _sed_file SED_FILE_PATH="runtimes/rust/src/deps/aws_cryptography_materialProviders.rs" \
8893
SED_BEFORE_STRING=' \#\[cfg(feature = "wrapped-client")\]' SED_AFTER_STRING='\/\/ Removed cfg(feature = "wrapped-client")'
94+
95+
# Python
96+
97+
PYTHON_MODULE_NAME=dbesdk_ddb_test_vectors
98+
99+
TRANSLATION_RECORD_PYTHON := \
100+
--translation-record ../submodules/MaterialProviders/StandardLibrary/runtimes/python/src/smithy_dafny_standard_library/internaldafny/generated/dafny_src-py.dtr \
101+
--translation-record ../submodules/MaterialProviders/ComAmazonawsKms/runtimes/python/src/aws_cryptography_internal_kms/internaldafny/generated/dafny_src-py.dtr \
102+
--translation-record ../submodules/MaterialProviders/ComAmazonawsDynamodb/runtimes/python/src/aws_cryptography_internal_dynamodb/internaldafny/generated/dafny_src-py.dtr \
103+
--translation-record ../submodules/MaterialProviders/AwsCryptographyPrimitives/runtimes/python/src/aws_cryptography_primitives/internaldafny/generated/dafny_src-py.dtr \
104+
--translation-record ../submodules/MaterialProviders/AwsCryptographicMaterialProviders/runtimes/python/src/aws_cryptographic_material_providers/internaldafny/generated/dafny_src-py.dtr \
105+
--translation-record ../submodules/MaterialProviders/TestVectorsAwsCryptographicMaterialProviders/runtimes/python/src/aws_cryptography_materialproviders_test_vectors/internaldafny/generated/dafny_src-py.dtr \
106+
--translation-record ../DynamoDbEncryption/runtimes/python/src/aws_database_encryption_sdk/internaldafny/generated/dafny_src-py.dtr
107+
108+
PYTHON_DEPENDENCY_MODULE_NAMES := \
109+
--dependency-library-name=aws.cryptography.primitives=aws_cryptography_primitives \
110+
--dependency-library-name=com.amazonaws.kms=aws_cryptography_internal_kms \
111+
--dependency-library-name=com.amazonaws.dynamodb=aws_cryptography_internal_dynamodb \
112+
--dependency-library-name=aws.cryptography.materialProviders=aws_cryptographic_material_providers \
113+
--dependency-library-name=aws.cryptography.keyStore=aws_cryptographic_material_providers \
114+
--dependency-library-name=aws.cryptography.materialProvidersTestVectorKeys=aws_cryptography_materialproviders_test_vectors \
115+
--dependency-library-name=aws.cryptography.dbEncryptionSdk.structuredEncryption=aws_database_encryption_sdk \
116+
--dependency-library-name=aws.cryptography.dbEncryptionSdk.dynamoDb=aws_database_encryption_sdk \
117+
--dependency-library-name=aws.cryptography.dbEncryptionSdk.dynamoDb.itemEncryptor=aws_database_encryption_sdk \
118+
--dependency-library-name=aws.cryptography.dbEncryptionSdk.dynamoDb.transforms=aws_database_encryption_sdk \
119+
120+
# Constants for languages that drop extern names (Python, Go)
121+
122+
INDEX_FILE_PATH=dafny/DDBEncryption/src/LibraryIndex.dfy
123+
INDEX_FILE_WITH_EXTERN_STRING="module {:extern \"software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.wrapped\"} WrappedDynamoDbEncryption refines WrappedAbstractAwsCryptographyDynamoDbEncryptionService"
124+
INDEX_FILE_WITHOUT_EXTERN_STRING="module WrappedDynamoDbEncryption refines WrappedAbstractAwsCryptographyDynamoDbEncryptionService"
125+
126+
_sed_types_file_remove_extern:
127+
echo "no types file"
128+
129+
_sed_types_file_add_extern:
130+
echo "no types file"

TestVectors/dafny/DDBEncryption/src/LibraryIndex.dfy

Lines changed: 1 addition & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -3,9 +3,7 @@
33

44
include "../Model/AwsCryptographyDynamoDbEncryptionTypesWrapped.dfy"
55

6-
module
7-
{:extern "software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.wrapped"}
8-
WrappedDynamoDbEncryption refines WrappedAbstractAwsCryptographyDynamoDbEncryptionService
6+
module {:extern "software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.wrapped"} WrappedDynamoDbEncryption refines WrappedAbstractAwsCryptographyDynamoDbEncryptionService
97
{
108

119
import WrappedService = DynamoDbEncryption

TestVectors/dafny/DDBEncryption/src/TestVectors.dfy

Lines changed: 30 additions & 30 deletions
Original file line numberDiff line numberDiff line change
@@ -83,36 +83,36 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
8383
}
8484

8585
var _ :- expect DecryptManifest.Decrypt("decrypt_dotnet_32.json");
86-
var _ :- expect DecryptManifest.Decrypt("decrypt_java_32.json");
87-
var _ :- expect DecryptManifest.Decrypt("decrypt_dotnet_33.json");
88-
var _ :- expect DecryptManifest.Decrypt("decrypt_java_33.json");
89-
var _ :- expect DecryptManifest.Decrypt("decrypt_dotnet_33a.json");
90-
var _ :- expect DecryptManifest.Decrypt("decrypt_java_33a.json");
91-
var _ :- expect WriteManifest.Write("encrypt.json");
92-
var _ :- expect EncryptManifest.Encrypt("encrypt.json", "decrypt.json", "java", "3.3");
93-
var _ :- expect DecryptManifest.Decrypt("decrypt.json");
94-
if |globalRecords| + |tableEncryptionConfigs| + |queries| == 0 {
95-
print "\nRunning no tests\n";
96-
return;
97-
}
98-
Validate();
99-
// Because of Dafny-Rust's lack of modules, there is no way to mae an interceptor for the wrapped DB-ESDK client.
100-
// So we create runtimes/rust/SkipLocal.txt to skip those tests that need the wrapped client.
101-
var skipLocal := FileIO.ReadBytesFromFile("SkipLocal.txt");
102-
if skipLocal.Success? {
103-
return;
104-
}
105-
StringOrdering();
106-
BasicIoTest();
107-
RunIoTests();
108-
BasicQueryTest();
109-
ConfigModTest();
110-
ComplexTests();
111-
WriteTests();
112-
RoundTripTests();
113-
DecryptTests();
114-
var client :- expect CreateInterceptedDDBClient.CreateVanillaDDBClient();
115-
DeleteTable(client);
86+
// var _ :- expect DecryptManifest.Decrypt("decrypt_java_32.json");
87+
// var _ :- expect DecryptManifest.Decrypt("decrypt_dotnet_33.json");
88+
// var _ :- expect DecryptManifest.Decrypt("decrypt_java_33.json");
89+
// var _ :- expect DecryptManifest.Decrypt("decrypt_dotnet_33a.json");
90+
// var _ :- expect DecryptManifest.Decrypt("decrypt_java_33a.json");
91+
// var _ :- expect WriteManifest.Write("encrypt.json");
92+
// var _ :- expect EncryptManifest.Encrypt("encrypt.json", "decrypt.json", "java", "3.3");
93+
// var _ :- expect DecryptManifest.Decrypt("decrypt.json");
94+
// if |globalRecords| + |tableEncryptionConfigs| + |queries| == 0 {
95+
// print "\nRunning no tests\n";
96+
// return;
97+
// }
98+
// Validate();
99+
// // Because of Dafny-Rust's lack of modules, there is no way to mae an interceptor for the wrapped DB-ESDK client.
100+
// // So we create runtimes/rust/SkipLocal.txt to skip those tests that need the wrapped client.
101+
// var skipLocal := FileIO.ReadBytesFromFile("SkipLocal.txt");
102+
// if skipLocal.Success? {
103+
// return;
104+
// }
105+
// StringOrdering();
106+
// BasicIoTest();
107+
// RunIoTests();
108+
// BasicQueryTest();
109+
// ConfigModTest();
110+
// ComplexTests();
111+
// WriteTests();
112+
// RoundTripTests();
113+
// DecryptTests();
114+
// var client :- expect CreateInterceptedDDBClient.CreateVanillaDDBClient();
115+
// DeleteTable(client);
116116
}
117117

118118
function NewOrderRecord(i : nat, str : string) : Record

0 commit comments

Comments
 (0)