Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/Index.dfy
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,7 @@ include "AwsEncryptionSdkOperations.dfy"

module
{:extern "software.amazon.cryptography.encryptionsdk.internaldafny" }
EncryptionSdk refines AbstractAwsCryptographyEncryptionSdkService {
ESDK refines AbstractAwsCryptographyEncryptionSdkService {
import Operations = AwsEncryptionSdkOperations
import Primitives = AtomicPrimitives
import MaterialProviders
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,7 @@ include "../src/Index.dfy"
module TestCreateEsdkClient {
import Types = AwsCryptographyEncryptionSdkTypes
import mplTypes = AwsCryptographyMaterialProvidersTypes
import EncryptionSdk
import ESDK
import MaterialProviders
import opened Wrappers
import opened UInt = StandardLibrary.UInt
Expand Down Expand Up @@ -50,11 +50,11 @@ module TestCreateEsdkClient {
];

method {:test} TestClientCreation() {
var defaultConfig := EncryptionSdk.DefaultAwsEncryptionSdkConfig();
var defaultConfig := ESDK.DefaultAwsEncryptionSdkConfig();

var esdk: Types.IAwsEncryptionSdkClient :- expect EncryptionSdk.ESDK(config := defaultConfig);
expect esdk is EncryptionSdk.ESDKClient;
var esdkClient := esdk as EncryptionSdk.ESDKClient;
var esdk: Types.IAwsEncryptionSdkClient :- expect ESDK.ESDK(config := defaultConfig);
expect esdk is ESDK.ESDKClient;
var esdkClient := esdk as ESDK.ESDKClient;

expect esdkClient.config.commitmentPolicy == defaultConfig.commitmentPolicy.value;
expect esdkClient.config.maxEncryptedDataKeys == defaultConfig.maxEncryptedDataKeys;
Expand Down Expand Up @@ -82,7 +82,7 @@ module TestCreateEsdkClient {
netV4_0_0_RetryPolicy := Some(Types.NetV4_0_0_RetryPolicy.FORBID_RETRY)
);

var noRetryEsdk :- expect EncryptionSdk.ESDK(config := esdkConfig);
var noRetryEsdk :- expect ESDK.ESDK(config := esdkConfig);

var expectFailureDecryptOutput := noRetryEsdk.Decrypt(Types.DecryptInput(
ciphertext := ESDK_NET_V400_MESSAGE,
Expand All @@ -95,8 +95,8 @@ module TestCreateEsdkClient {

// Decrypt v4.0.0 message with the default configuration which is to retry
// and expect decryption to pass
var defaultConfig := EncryptionSdk.DefaultAwsEncryptionSdkConfig();
var esdk :- expect EncryptionSdk.ESDK(config := defaultConfig);
var defaultConfig := ESDK.DefaultAwsEncryptionSdkConfig();
var esdk :- expect ESDK.ESDK(config := defaultConfig);

var decryptOutput := esdk.Decrypt(Types.DecryptInput(
ciphertext := ESDK_NET_V400_MESSAGE,
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,7 @@ module TestEncryptDecrypt {
import Types = AwsCryptographyEncryptionSdkTypes
import mplTypes = AwsCryptographyMaterialProvidersTypes
import MaterialProviders
import EncryptionSdk
import ESDK
import opened Wrappers

import Fixtures
Expand All @@ -20,8 +20,8 @@ module TestEncryptDecrypt {
// The string "asdf" as bytes
var asdf := [ 97, 115, 100, 102 ];

var defaultConfig := EncryptionSdk.DefaultAwsEncryptionSdkConfig();
var esdk :- expect EncryptionSdk.ESDK(config := defaultConfig);
var defaultConfig := ESDK.DefaultAwsEncryptionSdkConfig();
var esdk :- expect ESDK.ESDK(config := defaultConfig);
var mpl :- expect MaterialProviders.MaterialProviders();
var clientSupplier :- expect mpl.CreateDefaultClientSupplier(mplTypes.CreateDefaultClientSupplierInput);
var kmsClient :- expect clientSupplier.GetClient(mplTypes.GetClientInput(region := "us-west-2"));
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,7 @@ module TestReproducedEncryptionContext {
import Types = AwsCryptographyEncryptionSdkTypes
import mplTypes = AwsCryptographyMaterialProvidersTypes
import MaterialProviders
import EncryptionSdk
import ESDK
import opened Wrappers

import Fixtures
Expand All @@ -20,8 +20,8 @@ module TestReproducedEncryptionContext {
// The string "asdf" as bytes
var asdf := [ 97, 115, 100, 102 ];

var defaultConfig := EncryptionSdk.DefaultAwsEncryptionSdkConfig();
var esdk :- expect EncryptionSdk.ESDK(config := defaultConfig);
var defaultConfig := ESDK.DefaultAwsEncryptionSdkConfig();
var esdk :- expect ESDK.ESDK(config := defaultConfig);
var mpl :- expect MaterialProviders.MaterialProviders();
var clientSupplier :- expect mpl.CreateDefaultClientSupplier(mplTypes.CreateDefaultClientSupplierInput);
var kmsClient :- expect clientSupplier.GetClient(mplTypes.GetClientInput(region := "us-west-2"));
Expand Down Expand Up @@ -67,8 +67,8 @@ module TestReproducedEncryptionContext {
// The string "asdf" as bytes
var asdf := [ 97, 115, 100, 102 ];

var defaultConfig := EncryptionSdk.DefaultAwsEncryptionSdkConfig();
var esdk :- expect EncryptionSdk.ESDK(config := defaultConfig);
var defaultConfig := ESDK.DefaultAwsEncryptionSdkConfig();
var esdk :- expect ESDK.ESDK(config := defaultConfig);
var mpl :- expect MaterialProviders.MaterialProviders();
var clientSupplier :- expect mpl.CreateDefaultClientSupplier(mplTypes.CreateDefaultClientSupplierInput);
var kmsClient :- expect clientSupplier.GetClient(mplTypes.GetClientInput(region := "us-west-2"));
Expand Down Expand Up @@ -113,8 +113,8 @@ module TestReproducedEncryptionContext {
var asdf := [ 97, 115, 100, 102 ];

var namespace, name := Fixtures.NamespaceAndName(0);
var defaultConfig := EncryptionSdk.DefaultAwsEncryptionSdkConfig();
var esdk :- expect EncryptionSdk.ESDK(config := defaultConfig);
var defaultConfig := ESDK.DefaultAwsEncryptionSdkConfig();
var esdk :- expect ESDK.ESDK(config := defaultConfig);
var mpl :- expect MaterialProviders.MaterialProviders();
var rawAESKeyring :- expect mpl.CreateRawAesKeyring(mplTypes.CreateRawAesKeyringInput(
keyNamespace := namespace,
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -16,7 +16,7 @@ module TestRequiredEncryptionContext {
import KMS = Com.Amazonaws.Kms
import DDB = Com.Amazonaws.Dynamodb
import DDBTypes = ComAmazonawsDynamodbTypes
import EncryptionSdk
import ESDK
import opened Wrappers
import UTF8

Expand All @@ -35,8 +35,8 @@ module TestRequiredEncryptionContext {
// The string "asdf" as bytes
var asdf := [ 97, 115, 100, 102 ];

var defaultConfig := EncryptionSdk.DefaultAwsEncryptionSdkConfig();
var esdk :- expect EncryptionSdk.ESDK(config := defaultConfig);
var defaultConfig := ESDK.DefaultAwsEncryptionSdkConfig();
var esdk :- expect ESDK.ESDK(config := defaultConfig);
var mpl :- expect MaterialProviders.MaterialProviders();

// get keyrings
Expand Down Expand Up @@ -120,8 +120,8 @@ module TestRequiredEncryptionContext {
// The string "asdf" as bytes
var asdf := [ 97, 115, 100, 102 ];

var defaultConfig := EncryptionSdk.DefaultAwsEncryptionSdkConfig();
var esdk :- expect EncryptionSdk.ESDK(config := defaultConfig);
var defaultConfig := ESDK.DefaultAwsEncryptionSdkConfig();
var esdk :- expect ESDK.ESDK(config := defaultConfig);
var mpl :- expect MaterialProviders.MaterialProviders();

// get keyrings
Expand Down Expand Up @@ -229,8 +229,8 @@ module TestRequiredEncryptionContext {
// The string "asdf" as bytes
var asdf := [ 97, 115, 100, 102 ];

var defaultConfig := EncryptionSdk.DefaultAwsEncryptionSdkConfig();
var esdk :- expect EncryptionSdk.ESDK(config := defaultConfig);
var defaultConfig := ESDK.DefaultAwsEncryptionSdkConfig();
var esdk :- expect ESDK.ESDK(config := defaultConfig);
var mpl :- expect MaterialProviders.MaterialProviders();

// get keyrings
Expand Down Expand Up @@ -411,8 +411,8 @@ module TestRequiredEncryptionContext {
// The string "asdf" as bytes
var asdf := [ 97, 115, 100, 102 ];

var defaultConfig := EncryptionSdk.DefaultAwsEncryptionSdkConfig();
var esdk :- expect EncryptionSdk.ESDK(config := defaultConfig);
var defaultConfig := ESDK.DefaultAwsEncryptionSdkConfig();
var esdk :- expect ESDK.ESDK(config := defaultConfig);
var mpl :- expect MaterialProviders.MaterialProviders();

// get keyrings
Expand Down Expand Up @@ -586,8 +586,8 @@ module TestRequiredEncryptionContext {
// The string "asdf" as bytes
var asdf := [ 97, 115, 100, 102 ];

var defaultConfig := EncryptionSdk.DefaultAwsEncryptionSdkConfig();
var esdk :- expect EncryptionSdk.ESDK(config := defaultConfig);
var defaultConfig := ESDK.DefaultAwsEncryptionSdkConfig();
var esdk :- expect ESDK.ESDK(config := defaultConfig);
var mpl :- expect MaterialProviders.MaterialProviders();

// get keyrings
Expand Down Expand Up @@ -711,8 +711,8 @@ module TestRequiredEncryptionContext {
// The string "asdf" as bytes
var asdf := [ 97, 115, 100, 102 ];

var defaultConfig := EncryptionSdk.DefaultAwsEncryptionSdkConfig();
var esdk :- expect EncryptionSdk.ESDK(config := defaultConfig);
var defaultConfig := ESDK.DefaultAwsEncryptionSdkConfig();
var esdk :- expect ESDK.ESDK(config := defaultConfig);
var mpl :- expect MaterialProviders.MaterialProviders();

// get keyrings
Expand Down Expand Up @@ -814,8 +814,8 @@ module TestRequiredEncryptionContext {
// The string "asdf" as bytes
var asdf := [ 97, 115, 100, 102 ];

var defaultConfig := EncryptionSdk.DefaultAwsEncryptionSdkConfig();
var esdk :- expect EncryptionSdk.ESDK(config := defaultConfig);
var defaultConfig := ESDK.DefaultAwsEncryptionSdkConfig();
var esdk :- expect ESDK.ESDK(config := defaultConfig);
var mpl :- expect MaterialProviders.MaterialProviders();

// get keyrings
Expand Down Expand Up @@ -918,8 +918,8 @@ module TestRequiredEncryptionContext {
// The string "asdf" as bytes
var asdf := [ 97, 115, 100, 102 ];

var defaultConfig := EncryptionSdk.DefaultAwsEncryptionSdkConfig();
var esdk :- expect EncryptionSdk.ESDK(config := defaultConfig);
var defaultConfig := ESDK.DefaultAwsEncryptionSdkConfig();
var esdk :- expect ESDK.ESDK(config := defaultConfig);
var mpl :- expect MaterialProviders.MaterialProviders();

// get keyrings
Expand Down Expand Up @@ -1018,8 +1018,8 @@ module TestRequiredEncryptionContext {
// The string "asdf" as bytes
var asdf := [ 97, 115, 100, 102 ];

var defaultConfig := EncryptionSdk.DefaultAwsEncryptionSdkConfig();
var esdk :- expect EncryptionSdk.ESDK(config := defaultConfig);
var defaultConfig := ESDK.DefaultAwsEncryptionSdkConfig();
var esdk :- expect ESDK.ESDK(config := defaultConfig);
var mpl :- expect MaterialProviders.MaterialProviders();

// get keyrings
Expand Down Expand Up @@ -1133,8 +1133,8 @@ module TestRequiredEncryptionContext {
ensures output.ValidState() && fresh(output) && fresh(output.History) && fresh(output.Modifies)
{
var kmsKey := Fixtures.keyArn;
var defaultConfig := EncryptionSdk.DefaultAwsEncryptionSdkConfig();
var esdk :- expect EncryptionSdk.ESDK(config := defaultConfig);
var defaultConfig := ESDK.DefaultAwsEncryptionSdkConfig();
var esdk :- expect ESDK.ESDK(config := defaultConfig);
var mpl :- expect MaterialProviders.MaterialProviders();
var clientSupplier :- expect mpl.CreateDefaultClientSupplier(mplTypes.CreateDefaultClientSupplierInput);
var kmsClient :- expect clientSupplier.GetClient(mplTypes.GetClientInput(region := "us-west-2"));
Expand Down
2 changes: 1 addition & 1 deletion TestVectors/dafny/TestVectors/src/LibraryIndex.dfy
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,7 @@ module
{:extern "software.amazon.cryptography.encryptionsdk.internaldafny.wrapped" }
WrappedESDK refines WrappedAbstractAwsCryptographyEncryptionSdkService
{
import WrappedService = EncryptionSdk
import WrappedService = ESDK

function method WrappedDefaultAwsEncryptionSdkConfig(): AwsEncryptionSdkConfig
{
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,7 @@ module {:options "/functionSyntax:4"} AllEsdkV4NoReqEc {
import Types = AwsCryptographyEncryptionSdkTypes
import mplTypes = AwsCryptographyMaterialProvidersTypes
import keyVectorKeyTypes = AwsCryptographyMaterialProvidersTestVectorKeysTypes
import EncryptionSdk
import ESDK
import MaterialProviders
import opened CompleteVectors
import opened KeyDescription
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,7 @@ include "../LibraryIndex.dfy"
module {:options "/functionSyntax:4" } AllEsdkV4WithReqEc {
import Types = AwsCryptographyEncryptionSdkTypes
import mplTypes = AwsCryptographyMaterialProvidersTypes
import EncryptionSdk
import ESDK
import MaterialProviders
import opened CompleteVectors
import opened KeyDescription
Expand Down
2 changes: 1 addition & 1 deletion TestVectors/dafny/TestVectors/src/WriteVectors.dfy
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,7 @@ include "WriteEsdkJsonManifests.dfy"
module {:options "-functionSyntax:4"} WriteVectors {
import Types = AwsCryptographyEncryptionSdkTypes
import mplTypes = AwsCryptographyMaterialProvidersTypes
import EncryptionSdk
import ESDK
import MaterialProviders
import opened CompleteVectors
import opened Wrappers
Expand Down
Loading