Skip to content

Commit 52a3fc6

Browse files
ajewellamzjosecorellaseebees
authored
feat: Basic Test vectors, not yet in CI (#201)
* feat: add test vectors --------- Co-authored-by: Jose Corella <[email protected]> Co-authored-by: seebees <[email protected]>
1 parent 7e2e6ac commit 52a3fc6

File tree

24 files changed

+4349
-0
lines changed

24 files changed

+4349
-0
lines changed

‎TestVectors/.gitignore

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,6 @@
1+
TestResults
2+
ImplementationFromDafny.cs
3+
TestsFromDafny.cs
4+
**/bin
5+
**/obj
6+
/runtimes/java/dafny

‎TestVectors/Makefile

Lines changed: 60 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,60 @@
1+
# Copyright Amazon.com Inc. or its affiliates. All Rights Reserved.
2+
# SPDX-License-Identifier: Apache-2.0
3+
4+
CORES=2
5+
6+
include ../SharedMakefile.mk
7+
8+
PROJECT_SERVICES := \
9+
DDBEncryption \
10+
11+
SMITHY_MODEL_ROOT := $(PROJECT_ROOT)/DynamoDbEncryption/dafny/DynamoDbEncryption/Model
12+
OUTPUT_LOCAL_SERVICE_DDBEncryption := --local-service-test
13+
14+
SERVICE_NAMESPACE_DDBEncryption=aws.cryptography.dbEncryptionSdk.dynamoDb
15+
16+
MAX_RESOURCE_COUNT=10000000
17+
# Order is important
18+
# In java they MUST be built
19+
# in the order they depend on each other
20+
PROJECT_DEPENDENCIES := \
21+
submodules/MaterialProviders/AwsCryptographyPrimitives \
22+
submodules/MaterialProviders/ComAmazonawsKms \
23+
submodules/MaterialProviders/ComAmazonawsDynamodb \
24+
submodules/MaterialProviders/AwsCryptographicMaterialProviders \
25+
submodules/MaterialProviders/TestVectorsAwsCryptographicMaterialProviders \
26+
DynamoDbEncryption \
27+
28+
# Since we are packaging projects differently, we cannot make assumptions
29+
# about where the files are located.
30+
# This is here to get unblocked but should be removed once we have migrated packages
31+
# to the new packaging format.
32+
PROJECT_INDEX := \
33+
submodules/MaterialProviders/AwsCryptographyPrimitives/src/Index.dfy \
34+
submodules/MaterialProviders/ComAmazonawsKms/src/Index.dfy \
35+
submodules/MaterialProviders/ComAmazonawsDynamodb/src/Index.dfy \
36+
submodules/MaterialProviders/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Index.dfy \
37+
submodules/MaterialProviders/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/src/Index.dfy \
38+
submodules/MaterialProviders/TestVectorsAwsCryptographicMaterialProviders/dafny/KeyVectors/src/Index.dfy \
39+
DynamoDbEncryption/dafny/StructuredEncryption/src/Index.dfy \
40+
DynamoDbEncryption/dafny/DynamoDbEncryption/src/Index.dfy \
41+
42+
STD_LIBRARY=submodules/MaterialProviders/StandardLibrary
43+
SMITHY_DEPS=submodules/MaterialProviders/model
44+
45+
DIR_STRUCTURE_V2=V2
46+
47+
# Dependencies for each local service
48+
SERVICE_DEPS_DDBEncryption := \
49+
submodules/MaterialProviders/AwsCryptographyPrimitives \
50+
submodules/MaterialProviders/ComAmazonawsKms \
51+
submodules/MaterialProviders/ComAmazonawsDynamodb \
52+
submodules/MaterialProviders/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders \
53+
submodules/MaterialProviders/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore \
54+
DynamoDbEncryption/dafny/StructuredEncryption \
55+
DynamoDbEncryption/dafny/DynamoDbEncryption \
56+
submodules/MaterialProviders/TestVectorsAwsCryptographicMaterialProviders/dafny/TestVectorsAwsCryptographicMaterialProviders \
57+
58+
59+
format_net:
60+
pushd runtimes/net && dotnet format && popd

‎TestVectors/dafny/DDBEncryption/Model/AwsCryptographyDbEncryptionSdkDynamoDbTypesWrapped.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 WrappedAbstractAwsCryptographyDbEncryptionSdkDynamoDbService {
7+
import opened Wrappers
8+
import opened StandardLibrary.UInt
9+
import opened UTF8
10+
import opened Types = AwsCryptographyDbEncryptionSdkDynamoDbTypes
11+
import WrappedService : AbstractAwsCryptographyDbEncryptionSdkDynamoDbService
12+
function method WrappedDefaultDynamoDbEncryptionConfig(): DynamoDbEncryptionConfig
13+
method {:extern} WrappedDynamoDbEncryption(config: DynamoDbEncryptionConfig := WrappedDefaultDynamoDbEncryptionConfig())
14+
returns (res: Result<IDynamoDbEncryptionClient, 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/DDBEncryption/Model/AwsCryptographyDynamoDbEncryptionTypesWrapped.dfy

Lines changed: 23 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,23 @@
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+
// BEGIN MANUAL EDIT
6+
include "../../../../DynamoDbEncryption/dafny/DynamoDbEncryption/src/Index.dfy"
7+
include "../../../../submodules/MaterialProviders/TestVectorsAwsCryptographicMaterialProviders/dafny/KeyVectors/src/Index.dfy"
8+
// END MANUAL EDIT
9+
abstract module WrappedAbstractAwsCryptographyDynamoDbEncryptionService {
10+
import opened Wrappers
11+
import opened StandardLibrary.UInt
12+
import opened UTF8
13+
import opened Types = AwsCryptographyDbEncryptionSdkDynamoDbTypes
14+
import WrappedService : AbstractAwsCryptographyDbEncryptionSdkDynamoDbService
15+
function method WrappedDefaultDynamoDbEncryptionConfig(): DynamoDbEncryptionConfig
16+
method {:extern} WrappedDynamoDbEncryption(config: DynamoDbEncryptionConfig := WrappedDefaultDynamoDbEncryptionConfig())
17+
returns (res: Result<IDynamoDbEncryptionClient, Error>)
18+
ensures res.Success? ==>
19+
&& fresh(res.value)
20+
&& fresh(res.value.Modifies)
21+
&& fresh(res.value.History)
22+
&& res.value.ValidState()
23+
}

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

Lines changed: 27 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,27 @@
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+
6+
module CreateInterceptedDDBClient {
7+
import opened Wrappers
8+
import AwsCryptographyDbEncryptionSdkDynamoDbTypes
9+
import ComAmazonawsDynamodbTypes
10+
11+
method {:extern} CreateInterceptedDDBClient(config: AwsCryptographyDbEncryptionSdkDynamoDbTypes.DynamoDbTablesEncryptionConfig)
12+
returns (output: Result<ComAmazonawsDynamodbTypes.IDynamoDBClient, AwsCryptographyDbEncryptionSdkDynamoDbTypes.Error>)
13+
ensures output.Success? ==>
14+
&& fresh(output.value)
15+
&& fresh(output.value.Modifies)
16+
&& fresh(output.value.History)
17+
&& output.value.ValidState()
18+
19+
method {:extern} CreateVanillaDDBClient()
20+
returns (output: Result<ComAmazonawsDynamodbTypes.IDynamoDBClient, AwsCryptographyDbEncryptionSdkDynamoDbTypes.Error>)
21+
ensures output.Success? ==>
22+
&& fresh(output.value)
23+
&& fresh(output.value.Modifies)
24+
&& fresh(output.value.History)
25+
&& output.value.ValidState()
26+
27+
}

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

Lines changed: 35 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,35 @@
1+
// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved.
2+
// SPDX-License-Identifier: Apache-2.0
3+
4+
include "LibraryIndex.dfy"
5+
include "TestVectors.dfy"
6+
7+
module WrappedDDBEncryptionMain {
8+
import opened Wrappers
9+
import opened DdbEncryptionTestVectors
10+
11+
import CreateInterceptedDDBClient
12+
import FileIO
13+
import JSON.API
14+
import opened JSONHelpers
15+
16+
method AddJson(prev : TestVectorConfig, file : string) returns (output : Result<TestVectorConfig, string>)
17+
{
18+
var configBv :- expect FileIO.ReadBytesFromFile(file);
19+
var configBytes := BvToBytes(configBv);
20+
var json :- expect API.Deserialize(configBytes);
21+
output := ParseTestVector(json, prev);
22+
if output.Failure? {
23+
print output.error, "\n";
24+
}
25+
}
26+
27+
method ASDF() {
28+
var config := MakeEmptyTestVector();
29+
config :- expect AddJson(config, "records.json");
30+
config :- expect AddJson(config, "configs.json");
31+
config :- expect AddJson(config, "data.json");
32+
config :- expect AddJson(config, "iotest.json");
33+
config.RunAllTests();
34+
}
35+
}

0 commit comments

Comments
 (0)