Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

chore: Rename EncryptionSdk Dafny module name #707

Merged
merged 5 commits into from
Dec 10, 2024
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