diff --git a/AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/AwsEncryptionSdkOperations.dfy b/AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/AwsEncryptionSdkOperations.dfy index 695b3379d..1a89973e7 100644 --- a/AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/AwsEncryptionSdkOperations.dfy +++ b/AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/AwsEncryptionSdkOperations.dfy @@ -17,7 +17,7 @@ include "Serialize/EncryptionContext.dfy" module AwsEncryptionSdkOperations refines AbstractAwsCryptographyEncryptionSdkOperations { - import Aws.Cryptography.Primitives + import Primitives = AtomicPrimitives import MPL = AwsCryptographyMaterialProvidersTypes import MaterialProviders import EncryptDecryptHelpers diff --git a/AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/EncryptDecrypt.dfy b/AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/EncryptDecrypt.dfy index 6a3762abe..5825b02cf 100644 --- a/AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/EncryptDecrypt.dfy +++ b/AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/EncryptDecrypt.dfy @@ -15,7 +15,7 @@ module EncryptDecryptHelpers { import Types = AwsCryptographyEncryptionSdkTypes import MPL = AwsCryptographyMaterialProvidersTypes import MaterialProviders - import Aws.Cryptography.Primitives + import Primitives = AtomicPrimitives import MessageBody import SerializableTypes import opened SerializeFunctions diff --git a/AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/Index.dfy b/AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/Index.dfy index cf46c3714..ab851b1a8 100644 --- a/AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/Index.dfy +++ b/AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/Index.dfy @@ -7,7 +7,7 @@ module {:extern "software.amazon.cryptography.encryptionsdk.internaldafny" } EncryptionSdk refines AbstractAwsCryptographyEncryptionSdkService { import Operations = AwsEncryptionSdkOperations - import Aws.Cryptography.Primitives + import Primitives = AtomicPrimitives import MaterialProviders import AwsCryptographyMaterialProvidersTypes diff --git a/AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/KeyDerivation.dfy b/AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/KeyDerivation.dfy index 2607f528c..2456f756e 100644 --- a/AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/KeyDerivation.dfy +++ b/AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/KeyDerivation.dfy @@ -12,7 +12,7 @@ module KeyDerivation { import Types = AwsCryptographyEncryptionSdkTypes import MPL = AwsCryptographyMaterialProvidersTypes import AwsCryptographyPrimitivesTypes - import Aws.Cryptography.Primitives + import Primitives = AtomicPrimitives import HeaderTypes import SerializableTypes diff --git a/AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/MessageBody.dfy b/AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/MessageBody.dfy index 68315907a..0c0199111 100644 --- a/AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/MessageBody.dfy +++ b/AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/MessageBody.dfy @@ -22,7 +22,7 @@ module MessageBody { import opened UInt = StandardLibrary.UInt import Types = AwsCryptographyEncryptionSdkTypes import MPL = AwsCryptographyMaterialProvidersTypes - import Aws.Cryptography.Primitives + import Primitives = AtomicPrimitives import Streams import UTF8 import SerializableTypes diff --git a/AwsEncryptionSDK/dafny/AwsEncryptionSdk/test/Fixtures.dfy b/AwsEncryptionSDK/dafny/AwsEncryptionSdk/test/Fixtures.dfy index b7edf42a6..a7d7d5652 100644 --- a/AwsEncryptionSDK/dafny/AwsEncryptionSdk/test/Fixtures.dfy +++ b/AwsEncryptionSDK/dafny/AwsEncryptionSdk/test/Fixtures.dfy @@ -9,7 +9,7 @@ module Fixtures { import primitivesTypes = AwsCryptographyPrimitivesTypes import mplTypes = AwsCryptographyMaterialProvidersTypes import opened UInt = StandardLibrary.UInt - import Aws.Cryptography.Primitives + import Primitives = AtomicPrimitives // The following are test resources that exist in tests accounts: diff --git a/mpl b/mpl index ea0fe508d..4f7e715d2 160000 --- a/mpl +++ b/mpl @@ -1 +1 @@ -Subproject commit ea0fe508dca214b9c9bdaf0fc21122e83971ef1b +Subproject commit 4f7e715d29459b0e637067066c0fec321e00cd9b