Skip to content

Commit dacae91

Browse files
remove redundant code
1 parent 02ba132 commit dacae91

File tree

8 files changed

+75
-46
lines changed

8 files changed

+75
-46
lines changed

TestVectors/Makefile

Lines changed: 4 additions & 18 deletions
Original file line numberDiff line numberDiff line change
@@ -64,9 +64,9 @@ PROJECT_INDEX := \
6464
submodules/MaterialProviders/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/src/Index.dfy \
6565
submodules/MaterialProviders/TestVectorsAwsCryptographicMaterialProviders/dafny/KeyVectors/src/Index.dfy \
6666
DynamoDbEncryption/dafny/StructuredEncryption/src/Index.dfy \
67-
DynamoDbEncryption/dafny/DynamoDbEncryption/src/Index.dfy \
6867
DynamoDbEncryption/dafny/DynamoDbItemEncryptor/src/Index.dfy \
6968
DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/Index.dfy \
69+
DynamoDbEncryption/dafny/DynamoDbEncryption/src/Index.dfy \
7070

7171
STD_LIBRARY=submodules/MaterialProviders/StandardLibrary
7272
SMITHY_DEPS=submodules/MaterialProviders/model
@@ -80,8 +80,10 @@ SERVICE_DEPS_DDBEncryption := \
8080
submodules/MaterialProviders/ComAmazonawsDynamodb \
8181
submodules/MaterialProviders/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders \
8282
submodules/MaterialProviders/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore \
83-
DynamoDbEncryption/dafny/StructuredEncryption \
83+
DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms \
8484
DynamoDbEncryption/dafny/DynamoDbEncryption \
85+
DynamoDbEncryption/dafny/DynamoDbItemEncryptor \
86+
DynamoDbEncryption/dafny/StructuredEncryption \
8587
submodules/MaterialProviders/TestVectorsAwsCryptographicMaterialProviders/dafny/TestVectorsAwsCryptographicMaterialProviders \
8688

8789
transpile_implementation_rust: _remove_wrapped_client_rust
@@ -141,19 +143,3 @@ purge_polymorph_code:
141143
runtimes/go/TestsFromDafny-go/awscryptographydbencryptionsdkdynamodbsmithygenerated \
142144
runtimes/go/TestsFromDafny-go/awscryptographydbencryptionsdkdynamodbsmithygeneratedtypes \
143145
runtimes/go/TestsFromDafny-go/WrappedAwsCryptographyDbEncryptionSdkDynamoDbService
144-
145-
146-
_transpile_implementation_all:
147-
@echo "No polymorphing of dependency"
148-
149-
_transpile_test_all:
150-
@echo "No polymorphing of dependency"
151-
152-
_transpile_dependencies:
153-
@echo "No polymorphing of dependency"
154-
155-
_transpile_dependencies_test:
156-
@echo "No polymorphing of dependency"
157-
158-
mvn_local_deploy_dependencies:
159-
@echo "No polymorphing of dependency"

TestVectors/runtimes/java/build.gradle.kts

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -92,10 +92,10 @@ dependencies {
9292
implementation("software.amazon.cryptography:aws-database-encryption-sdk-dynamodb:${ddbecVersion}")
9393
implementation("software.amazon.cryptography:TestAwsCryptographicMaterialProviders:${mplVersion}")
9494

95-
implementation(platform("software.amazon.awssdk:bom:2.26.25"))
95+
implementation(platform("software.amazon.awssdk:bom:2.30.18"))
9696
implementation("software.amazon.awssdk:dynamodb")
9797
implementation("software.amazon.awssdk:dynamodb-enhanced")
98-
implementation("software.amazon.awssdk:core:2.26.25")
98+
implementation("software.amazon.awssdk:core:2.30.18")
9999
implementation("software.amazon.awssdk:kms")
100100
testImplementation("com.amazonaws:DynamoDBLocal:2.+")
101101
// This is where we gather the SQLLite files to copy over
@@ -139,4 +139,4 @@ tasks.register<JavaExec>("runTests") {
139139
systemProperty("java.library.path", "build/libs")
140140
mainClass.set("TestsFromDafny")
141141
classpath = sourceSets["test"].runtimeClasspath
142-
}
142+
}

TestVectors/runtimes/java/data.json

Lines changed: 14 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,19 @@
11
{
22
"Strings": [
33
"",
4-
"abc"
4+
"abc",
5+
"𐀂abc",
6+
"abc𐀂",
7+
"퀀",
8+
"퀀𐀂",
9+
"",
10+
"﹌𐀂",
11+
"𐀂﹌",
12+
"𐀂퀀",
13+
"𐀁𐀁",
14+
"𠀂",
15+
"𐀁𐀂",
16+
"𐀂𐀁"
517
],
618
"RoundTripTest": {
719
"Configs": {
@@ -377,4 +389,4 @@
377389
]
378390
}
379391
]
380-
}
392+
}

TestVectors/runtimes/net/Generated/DDBEncryption/TypeConversion.cs

Lines changed: 35 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -489,25 +489,30 @@ public static software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafn
489489
public static AWS.Cryptography.DbEncryptionSDK.DynamoDb.SingleKeyStore FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S14_SingleKeyStore(software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types._ISingleKeyStore value)
490490
{
491491
software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.SingleKeyStore concrete = (software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.SingleKeyStore)value; AWS.Cryptography.DbEncryptionSDK.DynamoDb.SingleKeyStore converted = new AWS.Cryptography.DbEncryptionSDK.DynamoDb.SingleKeyStore(); converted.KeyId = (string)FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S14_SingleKeyStore__M5_keyId(concrete._keyId);
492-
converted.CacheTTL = (int)FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S14_SingleKeyStore__M8_cacheTTL(concrete._cacheTTL); return converted;
492+
converted.CacheTTL = (int)FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S14_SingleKeyStore__M8_cacheTTL(concrete._cacheTTL);
493+
if (concrete._cache.is_Some) converted.Cache = (AWS.Cryptography.MaterialProviders.CacheType)FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S14_SingleKeyStore__M5_cache(concrete._cache);
494+
if (concrete._partitionId.is_Some) converted.PartitionId = (string)FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S14_SingleKeyStore__M11_partitionId(concrete._partitionId); return converted;
493495
}
494496
public static software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types._ISingleKeyStore ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S14_SingleKeyStore(AWS.Cryptography.DbEncryptionSDK.DynamoDb.SingleKeyStore value)
495497
{
496498
value.Validate();
497-
498-
return new software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.SingleKeyStore(ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S14_SingleKeyStore__M5_keyId(value.KeyId), ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S14_SingleKeyStore__M8_cacheTTL(value.CacheTTL));
499+
AWS.Cryptography.MaterialProviders.CacheType var_cache = value.IsSetCache() ? value.Cache : (AWS.Cryptography.MaterialProviders.CacheType)null;
500+
string var_partitionId = value.IsSetPartitionId() ? value.PartitionId : (string)null;
501+
return new software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.SingleKeyStore(ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S14_SingleKeyStore__M5_keyId(value.KeyId), ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S14_SingleKeyStore__M8_cacheTTL(value.CacheTTL), ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S14_SingleKeyStore__M5_cache(var_cache), ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S14_SingleKeyStore__M11_partitionId(var_partitionId));
499502
}
500503
public static AWS.Cryptography.DbEncryptionSDK.DynamoDb.MultiKeyStore FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S13_MultiKeyStore(software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types._IMultiKeyStore value)
501504
{
502505
software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.MultiKeyStore concrete = (software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.MultiKeyStore)value; AWS.Cryptography.DbEncryptionSDK.DynamoDb.MultiKeyStore converted = new AWS.Cryptography.DbEncryptionSDK.DynamoDb.MultiKeyStore(); converted.KeyFieldName = (string)FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S13_MultiKeyStore__M12_keyFieldName(concrete._keyFieldName);
503506
converted.CacheTTL = (int)FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S13_MultiKeyStore__M8_cacheTTL(concrete._cacheTTL);
504-
if (concrete._cache.is_Some) converted.Cache = (AWS.Cryptography.MaterialProviders.CacheType)FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S13_MultiKeyStore__M5_cache(concrete._cache); return converted;
507+
if (concrete._cache.is_Some) converted.Cache = (AWS.Cryptography.MaterialProviders.CacheType)FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S13_MultiKeyStore__M5_cache(concrete._cache);
508+
if (concrete._partitionId.is_Some) converted.PartitionId = (string)FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S13_MultiKeyStore__M11_partitionId(concrete._partitionId); return converted;
505509
}
506510
public static software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types._IMultiKeyStore ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S13_MultiKeyStore(AWS.Cryptography.DbEncryptionSDK.DynamoDb.MultiKeyStore value)
507511
{
508512
value.Validate();
509513
AWS.Cryptography.MaterialProviders.CacheType var_cache = value.IsSetCache() ? value.Cache : (AWS.Cryptography.MaterialProviders.CacheType)null;
510-
return new software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.MultiKeyStore(ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S13_MultiKeyStore__M12_keyFieldName(value.KeyFieldName), ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S13_MultiKeyStore__M8_cacheTTL(value.CacheTTL), ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S13_MultiKeyStore__M5_cache(var_cache));
514+
string var_partitionId = value.IsSetPartitionId() ? value.PartitionId : (string)null;
515+
return new software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.MultiKeyStore(ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S13_MultiKeyStore__M12_keyFieldName(value.KeyFieldName), ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S13_MultiKeyStore__M8_cacheTTL(value.CacheTTL), ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S13_MultiKeyStore__M5_cache(var_cache), ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S13_MultiKeyStore__M11_partitionId(var_partitionId));
511516
}
512517
public static AWS.Cryptography.DbEncryptionSDK.DynamoDb.PartOnly FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S8_PartOnly(software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types._IPartOnly value)
513518
{
@@ -722,6 +727,22 @@ public static int ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dyna
722727
{
723728
return ToDafny_N6_smithy__N3_api__S7_Integer(value);
724729
}
730+
public static AWS.Cryptography.MaterialProviders.CacheType FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S14_SingleKeyStore__M5_cache(Wrappers_Compile._IOption<software.amazon.cryptography.materialproviders.internaldafny.types._ICacheType> value)
731+
{
732+
return value.is_None ? (AWS.Cryptography.MaterialProviders.CacheType)null : FromDafny_N3_aws__N12_cryptography__N17_materialProviders__S9_CacheType(value.Extract());
733+
}
734+
public static Wrappers_Compile._IOption<software.amazon.cryptography.materialproviders.internaldafny.types._ICacheType> ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S14_SingleKeyStore__M5_cache(AWS.Cryptography.MaterialProviders.CacheType value)
735+
{
736+
return value == null ? Wrappers_Compile.Option<software.amazon.cryptography.materialproviders.internaldafny.types._ICacheType>.create_None() : Wrappers_Compile.Option<software.amazon.cryptography.materialproviders.internaldafny.types._ICacheType>.create_Some(ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S9_CacheType((AWS.Cryptography.MaterialProviders.CacheType)value));
737+
}
738+
public static string FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S14_SingleKeyStore__M11_partitionId(Wrappers_Compile._IOption<Dafny.ISequence<char>> value)
739+
{
740+
return value.is_None ? (string)null : FromDafny_N6_smithy__N3_api__S6_String(value.Extract());
741+
}
742+
public static Wrappers_Compile._IOption<Dafny.ISequence<char>> ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S14_SingleKeyStore__M11_partitionId(string value)
743+
{
744+
return value == null ? Wrappers_Compile.Option<Dafny.ISequence<char>>.create_None() : Wrappers_Compile.Option<Dafny.ISequence<char>>.create_Some(ToDafny_N6_smithy__N3_api__S6_String((string)value));
745+
}
725746
public static string FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S13_MultiKeyStore__M12_keyFieldName(Dafny.ISequence<char> value)
726747
{
727748
return FromDafny_N6_smithy__N3_api__S6_String(value);
@@ -746,6 +767,14 @@ public static AWS.Cryptography.MaterialProviders.CacheType FromDafny_N3_aws__N12
746767
{
747768
return value == null ? Wrappers_Compile.Option<software.amazon.cryptography.materialproviders.internaldafny.types._ICacheType>.create_None() : Wrappers_Compile.Option<software.amazon.cryptography.materialproviders.internaldafny.types._ICacheType>.create_Some(ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S9_CacheType((AWS.Cryptography.MaterialProviders.CacheType)value));
748769
}
770+
public static string FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S13_MultiKeyStore__M11_partitionId(Wrappers_Compile._IOption<Dafny.ISequence<char>> value)
771+
{
772+
return value.is_None ? (string)null : FromDafny_N6_smithy__N3_api__S6_String(value.Extract());
773+
}
774+
public static Wrappers_Compile._IOption<Dafny.ISequence<char>> ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S13_MultiKeyStore__M11_partitionId(string value)
775+
{
776+
return value == null ? Wrappers_Compile.Option<Dafny.ISequence<char>>.create_None() : Wrappers_Compile.Option<Dafny.ISequence<char>>.create_Some(ToDafny_N6_smithy__N3_api__S6_String((string)value));
777+
}
749778
public static string FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S6_Shared__M5_other(Dafny.ISequence<char> value)
750779
{
751780
return FromDafny_N6_smithy__N3_api__S6_String(value);
@@ -1641,4 +1670,4 @@ public static software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafn
16411670
}
16421671
}
16431672
}
1644-
}
1673+
}

TestVectors/runtimes/rust/Cargo.toml

Lines changed: 9 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -7,17 +7,17 @@ rust-version = "1.81.0"
77
# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
88

99
[dependencies]
10-
aws-config = "1.5.11"
11-
aws-lc-rs = "1.12.0"
12-
aws-lc-sys = "0.24.0"
13-
aws-sdk-dynamodb = "1.56.0"
14-
aws-sdk-kms = "1.52.0"
10+
aws-config = "1.5.15"
11+
aws-lc-rs = "1.12.2"
12+
aws-lc-sys = "0.25.0"
13+
aws-sdk-dynamodb = "1.62.0"
14+
aws-sdk-kms = "1.57.0"
1515
aws-smithy-runtime-api = {version = "1.7.3", features = ["client"] }
16-
aws-smithy-types = "1.2.10"
16+
aws-smithy-types = "1.2.12"
1717
chrono = "0.4.39"
1818
cpu-time = "1.0.0"
19-
dafny_runtime = { path = "../../../submodules/MaterialProviders/smithy-dafny/TestModels/dafny-dependencies/dafny_runtime_rust"}
19+
dafny_runtime = { path = "../../../submodules/smithy-dafny/TestModels/dafny-dependencies/dafny_runtime_rust", features = ["sync"] }
2020
dashmap = "6.1.0"
2121
pem = "3.0.4"
22-
tokio = {version = "1.42.0", features = ["full"] }
23-
uuid = { version = "1.11.0", features = ["v4"] }
22+
tokio = {version = "1.43.0", features = ["full"] }
23+
uuid = { version = "1.12.1", features = ["v4"] }

TestVectors/runtimes/rust/SkipLocal.txt

Lines changed: 0 additions & 1 deletion
This file was deleted.

TestVectors/runtimes/rust/src/create_client.rs

Lines changed: 8 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -1,13 +1,13 @@
11
// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved.
22
// SPDX-License-Identifier: Apache-2.0
33

4-
use std::rc::Rc;
4+
use dafny_runtime::Rc;
55
use dafny_runtime::Object;
66
use crate::implementation_from_dafny::software::amazon::cryptography::services::dynamodb::internaldafny::types::IDynamoDBClient;
77
use crate::implementation_from_dafny::software::amazon::cryptography::dbencryptionsdk::dynamodb::internaldafny::types::Error;
88
use crate::implementation_from_dafny::_Wrappers_Compile;
99
use std::sync::LazyLock;
10-
// use crate::intercept::DbEsdkInterceptor;
10+
use crate::intercept::DbEsdkInterceptor;
1111

1212
static DAFNY_TOKIO_RUNTIME: LazyLock<tokio::runtime::Runtime> = LazyLock::new(|| {
1313
tokio::runtime::Builder::new_multi_thread()
@@ -24,6 +24,8 @@ impl _CreateInterceptedDDBClient_Compile::_default {
2424
pub fn CreateInterceptedDDBClient(config : &Rc<crate::implementation_from_dafny::software::amazon::cryptography::dbencryptionsdk::dynamodb::internaldafny::types::DynamoDbTablesEncryptionConfig>)
2525
-> Rc<_Wrappers_Compile::Result<Object<dyn IDynamoDBClient>, Rc<Error>>>
2626
{
27+
28+
let table_configs = crate::deps::aws_cryptography_dbEncryptionSdk_dynamoDb_transforms::conversions::dynamo_db_tables_encryption_config::_dynamo_db_tables_encryption_config::plain_from_dafny(config);
2729
let shared_config = DAFNY_TOKIO_RUNTIME.block_on(aws_config::load_defaults(
2830
aws_config::BehaviorVersion::v2024_03_28()));
2931

@@ -33,13 +35,13 @@ impl _CreateInterceptedDDBClient_Compile::_default {
3335
.build();
3436

3537
let dynamo_config = aws_sdk_dynamodb::config::Builder::from(&shared_config)
36-
// .interceptor(DbEsdkInterceptor::new(table_configs))
38+
.interceptor(DbEsdkInterceptor::new(table_configs).unwrap())
3739
.build();
3840
let inner = aws_sdk_dynamodb::Client::from_conf(dynamo_config);
3941

4042
let client = crate::deps::com_amazonaws_dynamodb::client::Client { inner };
4143
let dafny_client = ::dafny_runtime::upcast_object()(::dafny_runtime::object::new(client));
42-
std::rc::Rc::new(crate::r#_Wrappers_Compile::Result::Success {
44+
Rc::new(crate::r#_Wrappers_Compile::Result::Success {
4345
value: dafny_client,
4446
})
4547
}
@@ -56,9 +58,9 @@ impl _CreateInterceptedDDBClient_Compile::_default {
5658
let inner = aws_sdk_dynamodb::Client::new(&shared_config);
5759
let client = crate::deps::com_amazonaws_dynamodb::client::Client { inner };
5860
let dafny_client = ::dafny_runtime::upcast_object()(::dafny_runtime::object::new(client));
59-
std::rc::Rc::new(crate::r#_Wrappers_Compile::Result::Success {
61+
Rc::new(crate::r#_Wrappers_Compile::Result::Success {
6062
value: dafny_client,
6163
})
6264
}
6365

64-
}
66+
}

TestVectors/runtimes/rust/src/lib.rs

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -13,6 +13,7 @@ pub mod error;
1313
pub mod operation;
1414
pub mod types;
1515
pub mod validation;
16+
pub mod intercept;
1617

1718
#[cfg(feature = "wrapped-client")]
1819
pub mod wrapped;
@@ -64,4 +65,4 @@ pub mod storm_tracker;
6465
pub mod time;
6566
pub mod uuid;
6667

67-
pub mod create_client;
68+
pub mod create_client;

0 commit comments

Comments
 (0)