Skip to content

Commit c5f5b31

Browse files
author
Lucas McDonald
committed
m
1 parent 9d82567 commit c5f5b31

File tree

9 files changed

+1381
-1
lines changed

9 files changed

+1381
-1
lines changed

‎TestVectors/Makefile

Lines changed: 17 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
@@ -66,6 +69,8 @@ PROJECT_INDEX := \
6669
DynamoDbEncryption/dafny/DynamoDbItemEncryptor/src/Index.dfy \
6770
DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/Index.dfy \
6871
DynamoDbEncryption/dafny/DynamoDbEncryption/src/Index.dfy \
72+
DynamoDbEncryption/dafny/DynamoDbItemEncryptor/src/Index.dfy \
73+
DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/Index.dfy \
6974

7075
STD_LIBRARY=submodules/MaterialProviders/StandardLibrary
7176
SMITHY_DEPS=submodules/MaterialProviders/model
@@ -85,6 +90,17 @@ SERVICE_DEPS_DDBEncryption := \
8590
DynamoDbEncryption/dafny/StructuredEncryption \
8691
submodules/MaterialProviders/TestVectorsAwsCryptographicMaterialProviders/dafny/TestVectorsAwsCryptographicMaterialProviders \
8792

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

90106
_remove_wrapped_client_rust:

‎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: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,2 @@
1+
// Empty stub expected by Smithy-Dafny
2+
module WrappedItemEncryptor {}

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

Lines changed: 33 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,33 @@
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.model.DynamoDbItemEncryptorConfig;
6+
import software.amazon.cryptography.dbencryptionsdk.dynamodb.ToDafny;
7+
import software.amazon.cryptography.dbencryptionsdk.dynamodb.ToNative;
8+
import software.amazon.cryptography.services.dynamodb.internaldafny.types.IItemEncryptor;
9+
import software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.Error;
10+
import software.amazon.cryptography.services.dynamodb.internaldafny.Shim;
11+
12+
public class __default {
13+
14+
public static Result<IItemEncryptor, Error> CreateWrappedItemEncryptor(
15+
software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.DynamoDbItemEncryptorConfig config
16+
) {
17+
try {
18+
final DynamoDbItemEncryptorConfig nativeConfig =
19+
ToNative.DynamoDbItemEncryptorConfig(config);
20+
21+
final DynamoDbItemEncryptor itemEncryptor = DynamoDbItemEncryptor
22+
.builder()
23+
.DynamoDbItemEncryptorConfig(nativeConfig)
24+
.build();
25+
26+
final Shim wrappedEncryptor = new Shim(itemEncryptor);
27+
28+
return Result.create_Success(wrappedEncryptor);
29+
} catch (Exception e) {
30+
return Result.create_Failure(ToDafny.Error((RuntimeException) e));
31+
}
32+
}
33+
}

‎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+
}

‎TestVectors/runtimes/net/Extern/CreateWrappedItemEncryptor.cs

Lines changed: 25 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,25 @@
1+
using Amazon.Cryptography.DatabaseEncryptionSDK.DynamoDb.ItemEncryptor;
2+
using Amazon.Cryptography.DatabaseEncryptionSDK.Dynamodb;
3+
using Amazon.Cryptography.Services.Dynamodb.Internaldafny;
4+
using Amazon.Cryptography.Services.Dynamodb.Internaldafny.Types;
5+
using Wrappers_Compile;
6+
using _IError = software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types._IError;
7+
8+
namespace CreateWrappedItemEncryptor_Compile
9+
{
10+
public partial class __default
11+
{
12+
public static _IResult<IItemEncryptor, _IError> CreateWrappedItemEncryptor(
13+
software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types._IDynamoDbItemEncryptorConfig config)
14+
{
15+
var nativeConfig = AWS.Cryptography.DbEncryptionSDK.DynamoDb.Transforms.TypeConversion
16+
.FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S30_DynamoDbItemEncryptorConfig(
17+
config);
18+
19+
var itemEncryptor = DynamoDbItemEncryptor.Create(nativeConfig);
20+
var wrappedEncryptor = new Com.Amazonaws.Dynamodb.ItemEncryptorShim(itemEncryptor);
21+
22+
return new Result_Success<IItemEncryptor, _IError>(wrappedEncryptor);
23+
}
24+
}
25+
}

‎TestVectors/runtimes/net/Generated/WrappedDynamoDbItemEncryptor/DynamoDbItemEncryptorShim.cs

Lines changed: 88 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,88 @@
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+
using System;
5+
using System.Collections.Generic;
6+
using System.IO;
7+
using System.Linq;
8+
namespace AWS.Cryptography.DbEncryptionSDK.DynamoDb.ItemEncryptor.Wrapped
9+
{
10+
public class DynamoDbItemEncryptorShim : software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.internaldafny.types.IDynamoDbItemEncryptorClient
11+
{
12+
public AWS.Cryptography.DbEncryptionSDK.DynamoDb.ItemEncryptor.DynamoDbItemEncryptor _impl;
13+
public DynamoDbItemEncryptorShim(AWS.Cryptography.DbEncryptionSDK.DynamoDb.ItemEncryptor.DynamoDbItemEncryptor impl)
14+
{
15+
this._impl = impl;
16+
}
17+
public Wrappers_Compile._IResult<software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.internaldafny.types._IEncryptItemOutput, software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.internaldafny.types._IError> EncryptItem(software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.internaldafny.types._IEncryptItemInput request)
18+
{
19+
try
20+
{
21+
AWS.Cryptography.DbEncryptionSDK.DynamoDb.ItemEncryptor.EncryptItemInput unWrappedRequest = TypeConversion.FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__N13_itemEncryptor__S16_EncryptItemInput(request);
22+
AWS.Cryptography.DbEncryptionSDK.DynamoDb.ItemEncryptor.EncryptItemOutput wrappedResponse =
23+
this._impl.EncryptItem(unWrappedRequest);
24+
return Wrappers_Compile.Result<software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.internaldafny.types._IEncryptItemOutput, software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.internaldafny.types._IError>.create_Success(TypeConversion.ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__N13_itemEncryptor__S17_EncryptItemOutput(wrappedResponse));
25+
}
26+
catch (System.Exception ex)
27+
{
28+
return Wrappers_Compile.Result<software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.internaldafny.types._IEncryptItemOutput, software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.internaldafny.types._IError>.create_Failure(this.ConvertError(ex));
29+
}
30+
31+
}
32+
public Wrappers_Compile._IResult<software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.internaldafny.types._IDecryptItemOutput, software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.internaldafny.types._IError> DecryptItem(software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.internaldafny.types._IDecryptItemInput request)
33+
{
34+
try
35+
{
36+
AWS.Cryptography.DbEncryptionSDK.DynamoDb.ItemEncryptor.DecryptItemInput unWrappedRequest = TypeConversion.FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__N13_itemEncryptor__S16_DecryptItemInput(request);
37+
AWS.Cryptography.DbEncryptionSDK.DynamoDb.ItemEncryptor.DecryptItemOutput wrappedResponse =
38+
this._impl.DecryptItem(unWrappedRequest);
39+
return Wrappers_Compile.Result<software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.internaldafny.types._IDecryptItemOutput, software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.internaldafny.types._IError>.create_Success(TypeConversion.ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__N13_itemEncryptor__S17_DecryptItemOutput(wrappedResponse));
40+
}
41+
catch (System.Exception ex)
42+
{
43+
return Wrappers_Compile.Result<software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.internaldafny.types._IDecryptItemOutput, software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.internaldafny.types._IError>.create_Failure(this.ConvertError(ex));
44+
}
45+
46+
}
47+
private software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.internaldafny.types._IError ConvertError(System.Exception error)
48+
{
49+
switch (error.GetType().Namespace)
50+
{
51+
case "AWS.Cryptography.DbEncryptionSDK.StructuredEncryption":
52+
return software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.internaldafny.types.Error.create_AwsCryptographyDbEncryptionSdkStructuredEncryption(
53+
AWS.Cryptography.DbEncryptionSDK.StructuredEncryption.TypeConversion.ToDafny_CommonError(error)
54+
);
55+
case "AWS.Cryptography.DbEncryptionSDK.DynamoDb":
56+
return software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.internaldafny.types.Error.create_AwsCryptographyDbEncryptionSdkDynamoDb(
57+
AWS.Cryptography.DbEncryptionSDK.DynamoDb.TypeConversion.ToDafny_CommonError(error)
58+
);
59+
case "AWS.Cryptography.MaterialProviders":
60+
return software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.internaldafny.types.Error.create_AwsCryptographyMaterialProviders(
61+
AWS.Cryptography.MaterialProviders.TypeConversion.ToDafny_CommonError(error)
62+
);
63+
case "Com.Amazonaws.Dynamodb":
64+
return software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.internaldafny.types.Error.create_ComAmazonawsDynamodb(
65+
Com.Amazonaws.Dynamodb.TypeConversion.ToDafny_CommonError(error)
66+
);
67+
}
68+
switch (error)
69+
{
70+
case AWS.Cryptography.DbEncryptionSDK.DynamoDb.ItemEncryptor.DynamoDbItemEncryptorException e:
71+
return TypeConversion.ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__N13_itemEncryptor__S30_DynamoDbItemEncryptorException(e);
72+
73+
case CollectionOfErrors collectionOfErrors:
74+
return new software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.internaldafny.types.Error_CollectionOfErrors(
75+
Dafny.Sequence<software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.internaldafny.types._IError>
76+
.FromArray(
77+
collectionOfErrors.list.Select
78+
(x => TypeConversion.ToDafny_CommonError(x))
79+
.ToArray()),
80+
Dafny.Sequence<char>.FromString(collectionOfErrors.Message)
81+
);
82+
default:
83+
return new software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.internaldafny.types.Error_Opaque(error);
84+
85+
}
86+
}
87+
}
88+
}

0 commit comments

Comments
 (0)