Skip to content

Commit ba9caca

Browse files
lucasmcdonald3lucasmcdonald3
authored
chore(TestVectors): Test Smithy-generated ItemEncryptor (#1814)
1 parent 10f530b commit ba9caca

14 files changed

Lines changed: 1482 additions & 7 deletions

File tree

‎TestVectors/Makefile‎

Lines changed: 40 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -7,14 +7,17 @@ TRANSPILE_TESTS_IN_RUST=1
77
include ../SharedMakefile.mk
88

99
PROJECT_SERVICES := \
10-
DDBEncryption
10+
DDBEncryption \
11+
WrappedDynamoDbItemEncryptor
1112

1213
MAIN_SERVICE_FOR_RUST := DDBEncryption
1314

1415
SMITHY_MODEL_ROOT := $(PROJECT_ROOT)/DynamoDbEncryption/dafny/DynamoDbEncryption/Model
1516
OUTPUT_LOCAL_SERVICE_DDBEncryption := --local-service-test
17+
OUTPUT_LOCAL_SERVICE_WrappedDynamoDbItemEncryptor := --local-service-test
1618

1719
SERVICE_NAMESPACE_DDBEncryption=aws.cryptography.dbEncryptionSdk.dynamoDb
20+
SERVICE_NAMESPACE_WrappedDynamoDbItemEncryptor=aws.cryptography.dbEncryptionSdk.dynamoDb.itemEncryptor
1821

1922
MAX_RESOURCE_COUNT=10000000
2023
# Order is important
@@ -35,6 +38,7 @@ RUST_OTHER_FILES := \
3538
runtimes/rust/src/ddb.rs \
3639
runtimes/rust/src/concurrent_call.rs \
3740
runtimes/rust/src/create_client.rs \
41+
runtimes/rust/src/create_wrapped_item_encryptor.rs \
3842
runtimes/rust/src/dafny_libraries.rs \
3943
runtimes/rust/src/digest.rs \
4044
runtimes/rust/src/ecdh.rs \
@@ -66,6 +70,8 @@ PROJECT_INDEX := \
6670
DynamoDbEncryption/dafny/DynamoDbItemEncryptor/src/Index.dfy \
6771
DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/Index.dfy \
6872
DynamoDbEncryption/dafny/DynamoDbEncryption/src/Index.dfy \
73+
DynamoDbEncryption/dafny/DynamoDbItemEncryptor/src/Index.dfy \
74+
DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/Index.dfy \
6975

7076
STD_LIBRARY=submodules/MaterialProviders/StandardLibrary
7177
SMITHY_DEPS=submodules/MaterialProviders/model
@@ -85,8 +91,41 @@ SERVICE_DEPS_DDBEncryption := \
8591
DynamoDbEncryption/dafny/StructuredEncryption \
8692
submodules/MaterialProviders/TestVectorsAwsCryptographicMaterialProviders/dafny/TestVectorsAwsCryptographicMaterialProviders \
8793

94+
SERVICE_DEPS_WrappedDynamoDbItemEncryptor := \
95+
submodules/MaterialProviders/AwsCryptographyPrimitives \
96+
submodules/MaterialProviders/ComAmazonawsKms \
97+
submodules/MaterialProviders/ComAmazonawsDynamodb \
98+
submodules/MaterialProviders/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders \
99+
submodules/MaterialProviders/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore \
100+
DynamoDbEncryption/dafny/StructuredEncryption \
101+
DynamoDbEncryption/dafny/DynamoDbEncryption \
102+
DynamoDbEncryption/dafny/DynamoDbItemEncryptor \
103+
submodules/MaterialProviders/TestVectorsAwsCryptographicMaterialProviders/dafny/TestVectorsAwsCryptographicMaterialProviders \
104+
88105
transpile_implementation_rust: _remove_wrapped_client_rust
89106

90107
_remove_wrapped_client_rust:
91108
$(MAKE) _sed_file SED_FILE_PATH="runtimes/rust/src/deps/aws_cryptography_materialProviders.rs" \
92109
SED_BEFORE_STRING=' \#\[cfg(feature = "wrapped-client")\]' SED_AFTER_STRING='\/\/ Removed cfg(feature = "wrapped-client")'
110+
111+
REMOVE_WRAPPED_CLIENT_AFTER_POLYMORPH_RUST_PRIMITIVES=runtimes/rust/src/deps/aws_cryptography_primitives.rs
112+
REMOVE_WRAPPED_CLIENT_AFTER_POLYMORPH_RUST_KEYSTORE=runtimes/rust/src/deps/aws_cryptography_keyStore.rs
113+
REMOVE_WRAPPED_CLIENT_AFTER_POLYMORPH_RUST_DYNAMODB=runtimes/rust/src/deps/aws_cryptography_dbEncryptionSdk_dynamoDb_transforms.rs
114+
REMOVE_WRAPPED_CLIENT_AFTER_POLYMORPH_RUST_DYNAMODB_ITEM_ENCRYPTOR=runtimes/rust/src/deps/aws_cryptography_dbEncryptionSdk_dynamoDb_itemEncryptor.rs
115+
REMOVE_WRAPPED_CLIENT_AFTER_POLYMORPH_RUST_DYNAMODB_STRUCTURED_ENCRYPTION=runtimes/rust/src/deps/aws_cryptography_dbEncryptionSdk_structuredEncryption.rs
116+
REMOVE_WRAPPED_CLIENT_AFTER_POLYMORPH_RUST_FROM_1 = "\#\[cfg(feature = \"wrapped-client\")\]"
117+
REMOVE_WRAPPED_CLIENT_AFTER_POLYMORPH_RUST_FROM_2 := 'pub mod wrapped;'
118+
REMOVE_WRAPPED_CLIENT_AFTER_POLYMORPH_RUST_TO_1 := '\/\/ removed wrapped-client feature using sed;'
119+
REMOVE_WRAPPED_CLIENT_AFTER_POLYMORPH_RUST_TO_2 := '\/\/ removed wrapped module using sed;'
120+
121+
_polymorph_rust: _remove_wrapped_client_rust
122+
123+
_remove_wrapped_client_rust:
124+
$(MAKE) _sed_file SED_FILE_PATH=$(REMOVE_WRAPPED_CLIENT_AFTER_POLYMORPH_RUST_PRIMITIVES) SED_BEFORE_STRING=$(REMOVE_WRAPPED_CLIENT_AFTER_POLYMORPH_RUST_FROM_1) SED_AFTER_STRING=$(REMOVE_WRAPPED_CLIENT_AFTER_POLYMORPH_RUST_TO_1)
125+
$(MAKE) _sed_file SED_FILE_PATH=$(REMOVE_WRAPPED_CLIENT_AFTER_POLYMORPH_RUST_PRIMITIVES) SED_BEFORE_STRING=$(REMOVE_WRAPPED_CLIENT_AFTER_POLYMORPH_RUST_FROM_2) SED_AFTER_STRING=$(REMOVE_WRAPPED_CLIENT_AFTER_POLYMORPH_RUST_TO_2)
126+
$(MAKE) _sed_file SED_FILE_PATH=$(REMOVE_WRAPPED_CLIENT_AFTER_POLYMORPH_RUST_KEYSTORE) SED_BEFORE_STRING=$(REMOVE_WRAPPED_CLIENT_AFTER_POLYMORPH_RUST_FROM_1) SED_AFTER_STRING=$(REMOVE_WRAPPED_CLIENT_AFTER_POLYMORPH_RUST_TO_1)
127+
$(MAKE) _sed_file SED_FILE_PATH=$(REMOVE_WRAPPED_CLIENT_AFTER_POLYMORPH_RUST_KEYSTORE) SED_BEFORE_STRING=$(REMOVE_WRAPPED_CLIENT_AFTER_POLYMORPH_RUST_FROM_2) SED_AFTER_STRING=$(REMOVE_WRAPPED_CLIENT_AFTER_POLYMORPH_RUST_TO_2)
128+
$(MAKE) _sed_file SED_FILE_PATH=$(REMOVE_WRAPPED_CLIENT_AFTER_POLYMORPH_RUST_DYNAMODB) SED_BEFORE_STRING=$(REMOVE_WRAPPED_CLIENT_AFTER_POLYMORPH_RUST_FROM_1) SED_AFTER_STRING=$(REMOVE_WRAPPED_CLIENT_AFTER_POLYMORPH_RUST_TO_1)
129+
$(MAKE) _sed_file SED_FILE_PATH=$(REMOVE_WRAPPED_CLIENT_AFTER_POLYMORPH_RUST_DYNAMODB) SED_BEFORE_STRING=$(REMOVE_WRAPPED_CLIENT_AFTER_POLYMORPH_RUST_FROM_2) SED_AFTER_STRING=$(REMOVE_WRAPPED_CLIENT_AFTER_POLYMORPH_RUST_TO_2)
130+
$(MAKE) _sed_file SED_FILE_PATH=$(REMOVE_WRAPPED_CLIENT_AFTER_POLYMORPH_RUST_DYNAMODB_STRUCTURED_ENCRYPTION) SED_BEFORE_STRING=$(REMOVE_WRAPPED_CLIENT_AFTER_POLYMORPH_RUST_FROM_1) SED_AFTER_STRING=$(REMOVE_WRAPPED_CLIENT_AFTER_POLYMORPH_RUST_TO_1)
131+
$(MAKE) _sed_file SED_FILE_PATH=$(REMOVE_WRAPPED_CLIENT_AFTER_POLYMORPH_RUST_DYNAMODB_STRUCTURED_ENCRYPTION) SED_BEFORE_STRING=$(REMOVE_WRAPPED_CLIENT_AFTER_POLYMORPH_RUST_FROM_2) SED_AFTER_STRING=$(REMOVE_WRAPPED_CLIENT_AFTER_POLYMORPH_RUST_TO_2)

‎TestVectors/dafny/DDBEncryption/src/CreateWrappedItemEncryptor.dfy‎

Lines changed: 50 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,50 @@
1+
// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved.
2+
// SPDX-License-Identifier: Apache-2.0
3+
4+
include "../Model/AwsCryptographyDynamoDbEncryptionTypesWrapped.dfy"
5+
include "../../../../DynamoDbEncryption/dafny/DynamoDbItemEncryptor/src/Index.dfy"
6+
7+
module {:extern} CreateWrappedItemEncryptor {
8+
import opened Wrappers
9+
import AwsCryptographyDbEncryptionSdkDynamoDbTypes
10+
import ENC = AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorTypes
11+
import DynamoDbItemEncryptor
12+
import Operations = AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations
13+
14+
method {:extern} CreateWrappedItemEncryptor(config: ENC.DynamoDbItemEncryptorConfig)
15+
returns (output: Result<ENC.IDynamoDbItemEncryptorClient, ENC.Error>)
16+
ensures output.Success? ==>
17+
&& output.value is DynamoDbItemEncryptor.DynamoDbItemEncryptorClient
18+
&& fresh(output.value)
19+
&& fresh(output.value.History)
20+
&& output.value.ValidState()
21+
&& var rconfig := (output.value as DynamoDbItemEncryptor.DynamoDbItemEncryptorClient).config;
22+
&& fresh(output.value.Modifies)
23+
&& rconfig.logicalTableName == config.logicalTableName
24+
&& rconfig.partitionKeyName == config.partitionKeyName
25+
&& rconfig.sortKeyName == config.sortKeyName
26+
&& rconfig.attributeActionsOnEncrypt == config.attributeActionsOnEncrypt
27+
&& rconfig.allowedUnsignedAttributes == config.allowedUnsignedAttributes
28+
&& rconfig.allowedUnsignedAttributePrefix == config.allowedUnsignedAttributePrefix
29+
&& rconfig.algorithmSuiteId == config.algorithmSuiteId
30+
31+
//= specification/dynamodb-encryption-client/ddb-table-encryption-config.md#attribute-actions
32+
//= type=implication
33+
//# The [Key Action](#key-action)
34+
//# MUST be configured to the partition attribute and, if present, sort attribute.
35+
&& rconfig.version == Operations.VersionFromActions(config.attributeActionsOnEncrypt)
36+
&& config.partitionKeyName in config.attributeActionsOnEncrypt
37+
&& config.attributeActionsOnEncrypt[config.partitionKeyName] == Operations.KeyActionFromVersion(rconfig.version)
38+
&& (config.sortKeyName.Some? ==>
39+
&& config.sortKeyName.value in config.attributeActionsOnEncrypt
40+
&& config.attributeActionsOnEncrypt[config.sortKeyName.value] == Operations.KeyActionFromVersion(rconfig.version))
41+
42+
//= specification/dynamodb-encryption-client/ddb-table-encryption-config.md#plaintext-policy
43+
//# If not specified, encryption and decryption MUST behave according to `FORBID_PLAINTEXT_WRITE_FORBID_PLAINTEXT_READ`.
44+
ensures
45+
&& output.Success?
46+
&& config.plaintextOverride.None?
47+
==>
48+
&& var config := (output.value as DynamoDbItemEncryptor.DynamoDbItemEncryptorClient).config;
49+
&& config.plaintextOverride.FORBID_PLAINTEXT_WRITE_FORBID_PLAINTEXT_READ?
50+
}

‎TestVectors/dafny/DDBEncryption/src/Index.dfy‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -4,6 +4,7 @@
44
include "LibraryIndex.dfy"
55
include "TestVectors.dfy"
66
include "WriteSetPermutations.dfy"
7+
include "../../WrappedDynamoDbItemEncryptor/src/Index.dfy"
78

89
module WrappedDDBEncryptionMain {
910
import opened Wrappers
@@ -16,6 +17,7 @@ module WrappedDDBEncryptionMain {
1617
import opened JSONHelpers
1718
import KeyVectors
1819
import KeyVectorsTypes = AwsCryptographyMaterialProvidersTestVectorKeysTypes
20+
import WrappedItemEncryptor
1921

2022

2123
const DEFAULT_KEYS : string := "../../../submodules/MaterialProviders/TestVectorsAwsCryptographicMaterialProviders/dafny/TestVectorsAwsCryptographicMaterialProviders/test/keys.json"

‎TestVectors/dafny/DDBEncryption/src/JsonConfig.dfy‎

Lines changed: 6 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -3,6 +3,7 @@
33

44
include "JsonItem.dfy"
55
include "CreateInterceptedDDBClient.dfy"
6+
include "CreateWrappedItemEncryptor.dfy"
67
include "../../../../DynamoDbEncryption/dafny/DynamoDbItemEncryptor/src/Index.dfy"
78

89
module {:options "-functionSyntax:4"} JsonConfig {
@@ -31,6 +32,8 @@ module {:options "-functionSyntax:4"} JsonConfig {
3132
import ParseJsonManifests
3233
import CreateInterceptedDDBClient
3334
import DynamoDbItemEncryptor
35+
import CreateWrappedItemEncryptor
36+
import Operations = AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations
3437

3538

3639
const abc : UTF8.ValidUTF8Bytes :=
@@ -259,7 +262,7 @@ module {:options "-functionSyntax:4"} JsonConfig {
259262
}
260263

261264
method GetItemEncryptor(name : string, data : JSON, keys: KeyVectors.KeyVectorsClient)
262-
returns (encryptor : Result<DynamoDbItemEncryptor.DynamoDbItemEncryptorClient, string>)
265+
returns (encryptor : Result<ENC.IDynamoDbItemEncryptorClient, string>)
263266
requires keys.ValidState()
264267
modifies keys.Modifies
265268
ensures keys.ValidState()
@@ -357,10 +360,8 @@ module {:options "-functionSyntax:4"} JsonConfig {
357360
legacyOverride := legacyOverride,
358361
plaintextOverride := plaintextOverride
359362
);
360-
var enc : ENC.IDynamoDbItemEncryptorClient :- expect DynamoDbItemEncryptor.DynamoDbItemEncryptor(encryptorConfig);
361-
assert enc is DynamoDbItemEncryptor.DynamoDbItemEncryptorClient;
362-
var encr := enc as DynamoDbItemEncryptor.DynamoDbItemEncryptorClient;
363-
return Success(encr);
363+
var enc : ENC.IDynamoDbItemEncryptorClient :- expect CreateWrappedItemEncryptor.CreateWrappedItemEncryptor(encryptorConfig);
364+
return Success(enc);
364365
}
365366

366367
method GetOneTableConfig(name : string, data : JSON, keys: KeyVectors.KeyVectorsClient)

‎TestVectors/dafny/WrappedDynamoDbItemEncryptor/Model/AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorTypesWrapped.dfy‎

Lines changed: 20 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,20 @@
1+
// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved.
2+
// SPDX-License-Identifier: Apache-2.0
3+
// Do not modify this file. This file is machine generated, and any changes to it will be overwritten.
4+
include "../../../../submodules/MaterialProviders/StandardLibrary/src/Index.dfy"
5+
include "../src/Index.dfy"
6+
abstract module WrappedAbstractAwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorService {
7+
import opened Wrappers
8+
import opened StandardLibrary.UInt
9+
import opened UTF8
10+
import opened Types = AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorTypes
11+
import WrappedService : AbstractAwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorService
12+
function method WrappedDefaultDynamoDbItemEncryptorConfig(): DynamoDbItemEncryptorConfig
13+
method {:extern} WrappedDynamoDbItemEncryptor(config: DynamoDbItemEncryptorConfig := WrappedDefaultDynamoDbItemEncryptorConfig())
14+
returns (res: Result<IDynamoDbItemEncryptorClient, Error>)
15+
ensures res.Success? ==>
16+
&& fresh(res.value)
17+
&& fresh(res.value.Modifies)
18+
&& fresh(res.value.History)
19+
&& res.value.ValidState()
20+
}

‎TestVectors/dafny/WrappedDynamoDbItemEncryptor/src/Index.dfy‎

Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,15 @@
1+
// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved.
2+
// SPDX-License-Identifier: Apache-2.0
3+
// Empty stub expected by Smithy-Dafny
4+
5+
include "../../../../DynamoDbEncryption/dafny/DynamoDbItemEncryptor/src/Index.dfy"
6+
include "../Model/AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorTypesWrapped.dfy"
7+
module {:extern "software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.internaldafny.wrapped" } WrappedItemEncryptor refines WrappedAbstractAwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorService {
8+
9+
import DynamoDbItemEncryptor
10+
11+
function method WrappedDefaultDynamoDbItemEncryptorConfig(): DynamoDbItemEncryptorConfig
12+
{
13+
DynamoDbItemEncryptor.DefaultDynamoDbItemEncryptorConfig()
14+
}
15+
}

‎TestVectors/runtimes/java/src/main/java/CreateWrappedItemEncryptor_Compile/__default.java‎

Lines changed: 37 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,37 @@
1+
package CreateWrappedItemEncryptor_Compile;
2+
3+
import Wrappers_Compile.Result;
4+
import software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.DynamoDbItemEncryptor;
5+
import software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.ToDafny;
6+
import software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.ToNative;
7+
import software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.internaldafny.types.Error;
8+
import software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.internaldafny.types.IDynamoDbItemEncryptorClient;
9+
import software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.model.DynamoDbItemEncryptorConfig;
10+
import software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.wrapped.TestDynamoDbItemEncryptor;
11+
12+
public class __default {
13+
14+
public static Result<
15+
IDynamoDbItemEncryptorClient,
16+
Error
17+
> CreateWrappedItemEncryptor(
18+
software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.internaldafny.types.DynamoDbItemEncryptorConfig config
19+
) {
20+
try {
21+
final DynamoDbItemEncryptorConfig nativeConfig =
22+
ToNative.DynamoDbItemEncryptorConfig(config);
23+
24+
final DynamoDbItemEncryptor itemEncryptor = DynamoDbItemEncryptor
25+
.builder()
26+
.DynamoDbItemEncryptorConfig(nativeConfig)
27+
.build();
28+
29+
final TestDynamoDbItemEncryptor wrappedEncryptor =
30+
TestDynamoDbItemEncryptor.builder().impl(itemEncryptor).build();
31+
32+
return Result.create_Success(wrappedEncryptor);
33+
} catch (Exception e) {
34+
return Result.create_Failure(ToDafny.Error((RuntimeException) e));
35+
}
36+
}
37+
}

‎TestVectors/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/itemencryptor/wrapped/TestDynamoDbItemEncryptor.java‎

Lines changed: 110 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,110 @@
1+
// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved.
2+
// SPDX-License-Identifier: Apache-2.0
3+
// Do not modify this file. This file is machine generated, and any changes to it will be overwritten.
4+
package software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.wrapped;
5+
6+
import Wrappers_Compile.Result;
7+
import java.lang.IllegalArgumentException;
8+
import java.lang.RuntimeException;
9+
import java.util.Objects;
10+
import software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.DynamoDbItemEncryptor;
11+
import software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.ToDafny;
12+
import software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.ToNative;
13+
import software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.internaldafny.types.DecryptItemInput;
14+
import software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.internaldafny.types.DecryptItemOutput;
15+
import software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.internaldafny.types.EncryptItemInput;
16+
import software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.internaldafny.types.EncryptItemOutput;
17+
import software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.internaldafny.types.Error;
18+
import software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.internaldafny.types.IDynamoDbItemEncryptorClient;
19+
20+
public class TestDynamoDbItemEncryptor implements IDynamoDbItemEncryptorClient {
21+
22+
private final DynamoDbItemEncryptor _impl;
23+
24+
protected TestDynamoDbItemEncryptor(BuilderImpl builder) {
25+
this._impl = builder.impl();
26+
}
27+
28+
public static Builder builder() {
29+
return new BuilderImpl();
30+
}
31+
32+
public Result<DecryptItemOutput, Error> DecryptItem(
33+
DecryptItemInput dafnyInput
34+
) {
35+
try {
36+
software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.model.DecryptItemInput nativeInput =
37+
ToNative.DecryptItemInput(dafnyInput);
38+
software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.model.DecryptItemOutput nativeOutput =
39+
this._impl.DecryptItem(nativeInput);
40+
DecryptItemOutput dafnyOutput = ToDafny.DecryptItemOutput(nativeOutput);
41+
return Result.create_Success(
42+
DecryptItemOutput._typeDescriptor(),
43+
Error._typeDescriptor(),
44+
dafnyOutput
45+
);
46+
} catch (RuntimeException ex) {
47+
return Result.create_Failure(
48+
DecryptItemOutput._typeDescriptor(),
49+
Error._typeDescriptor(),
50+
ToDafny.Error(ex)
51+
);
52+
}
53+
}
54+
55+
public Result<EncryptItemOutput, Error> EncryptItem(
56+
EncryptItemInput dafnyInput
57+
) {
58+
try {
59+
software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.model.EncryptItemInput nativeInput =
60+
ToNative.EncryptItemInput(dafnyInput);
61+
software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.model.EncryptItemOutput nativeOutput =
62+
this._impl.EncryptItem(nativeInput);
63+
EncryptItemOutput dafnyOutput = ToDafny.EncryptItemOutput(nativeOutput);
64+
return Result.create_Success(
65+
EncryptItemOutput._typeDescriptor(),
66+
Error._typeDescriptor(),
67+
dafnyOutput
68+
);
69+
} catch (RuntimeException ex) {
70+
return Result.create_Failure(
71+
EncryptItemOutput._typeDescriptor(),
72+
Error._typeDescriptor(),
73+
ToDafny.Error(ex)
74+
);
75+
}
76+
}
77+
78+
public interface Builder {
79+
Builder impl(DynamoDbItemEncryptor impl);
80+
81+
DynamoDbItemEncryptor impl();
82+
83+
TestDynamoDbItemEncryptor build();
84+
}
85+
86+
static class BuilderImpl implements Builder {
87+
88+
protected DynamoDbItemEncryptor impl;
89+
90+
protected BuilderImpl() {}
91+
92+
public Builder impl(DynamoDbItemEncryptor impl) {
93+
this.impl = impl;
94+
return this;
95+
}
96+
97+
public DynamoDbItemEncryptor impl() {
98+
return this.impl;
99+
}
100+
101+
public TestDynamoDbItemEncryptor build() {
102+
if (Objects.isNull(this.impl())) {
103+
throw new IllegalArgumentException(
104+
"Missing value for required field `impl`"
105+
);
106+
}
107+
return new TestDynamoDbItemEncryptor(this);
108+
}
109+
}
110+
}

0 commit comments

Comments
 (0)