chore: Rename AtomicPrimitives Dafny module name

AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/AwsCryptographyMaterialProvidersOperations.dfy

@@ -55,7 +55,7 @@ module AwsCryptographyMaterialProvidersOperations refines AbstractAwsCryptograph
   import StormTracker
   import StormTrackingCMC
   import Crypto = AwsCryptographyPrimitivesTypes
-  import Aws.Cryptography.Primitives
+  import AtomicPrimitives
   import opened AwsKmsUtils
   import DefaultClientSupplier
   import Materials
@@ -68,7 +68,7 @@ module AwsCryptographyMaterialProvidersOperations refines AbstractAwsCryptograph
   import RequiredEncryptionContextCMM
 
   datatype Config = Config(
-    nameonly crypto: Primitives.AtomicPrimitivesClient
+    nameonly crypto: AtomicPrimitives.AtomicPrimitivesClient
   )
 
   type InternalConfig = Config

AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/CMMs/DefaultCMM.dfy

@@ -19,7 +19,7 @@ module DefaultCMM {
   import UTF8
   import Types = AwsCryptographyMaterialProvidersTypes
   import Crypto = AwsCryptographyPrimitivesTypes
-  import Aws.Cryptography.Primitives
+  import AtomicPrimitives
   import Defaults
   import Commitment
   import Seq
@@ -28,7 +28,7 @@ module DefaultCMM {
   class DefaultCMM
     extends CMM.VerifiableInterface
   {
-    const cryptoPrimitives: Primitives.AtomicPrimitivesClient
+    const cryptoPrimitives: AtomicPrimitives.AtomicPrimitivesClient
 
     predicate ValidState()
       ensures ValidState() ==> History in Modifies
@@ -51,7 +51,7 @@ module DefaultCMM {
       //# the caller MUST provide the following value:
       //# - [Keyring](#keyring)
       k: Types.IKeyring,
-      c: Primitives.AtomicPrimitivesClient
+      c: AtomicPrimitives.AtomicPrimitivesClient
     )
       requires k.ValidState() && c.ValidState()
       ensures keyring == k && cryptoPrimitives == c

AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Index.dfy

@@ -3,13 +3,11 @@
 
 include "AwsCryptographyMaterialProvidersOperations.dfy"
 
-module
-  {:extern "software.amazon.cryptography.materialproviders.internaldafny" }
-  MaterialProviders refines AbstractAwsCryptographyMaterialProvidersService
+module {:extern "software.amazon.cryptography.materialproviders.internaldafny" } MaterialProviders refines AbstractAwsCryptographyMaterialProvidersService
 {
 
   import Operations = AwsCryptographyMaterialProvidersOperations
-  import Aws.Cryptography.Primitives
+  import AtomicPrimitives
   import Crypto = AwsCryptographyPrimitivesTypes
 
   function method DefaultMaterialProvidersConfig(): MaterialProvidersConfig
@@ -22,11 +20,11 @@ module
     ensures res.Success? ==>
               && res.value is MaterialProvidersClient
   {
-    var maybeCrypto := Primitives.AtomicPrimitives();
+    var maybeCrypto := AtomicPrimitives.AtomicPrimitives();
     var cryptoPrimitivesX : Crypto.IAwsCryptographicPrimitivesClient :- maybeCrypto
     .MapFailure(e => Types.AwsCryptographyPrimitives(e));
-    assert cryptoPrimitivesX is Primitives.AtomicPrimitivesClient;
-    var cryptoPrimitives := cryptoPrimitivesX as Primitives.AtomicPrimitivesClient;
+    assert cryptoPrimitivesX is AtomicPrimitives.AtomicPrimitivesClient;
+    var cryptoPrimitives := cryptoPrimitivesX as AtomicPrimitives.AtomicPrimitivesClient;
 
     var client := new MaterialProvidersClient(Operations.Config( crypto := cryptoPrimitives ));
     return Success(client);

AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/KeyWrapping/EcdhEdkWrapping.dfy

@@ -20,7 +20,7 @@ module {:options "/functionSyntax:4" } EcdhEdkWrapping {
   import opened AlgorithmSuites
   import PrimitiveTypes = AwsCryptographyPrimitivesTypes
   import Types = AwsCryptographyMaterialProvidersTypes
-  import Aws.Cryptography.Primitives
+  import AtomicPrimitives
   import Materials
 
   datatype EcdhUnwrapInfo = EcdhUnwrapInfo()
@@ -34,15 +34,15 @@ module {:options "/functionSyntax:4" } EcdhEdkWrapping {
     const sharedSecret: seq<uint8>
     const keyringVersion: seq<uint8>
     const curveSpec: PrimitiveTypes.ECDHCurveSpec
-    const crypto: Primitives.AtomicPrimitivesClient
+    const crypto: AtomicPrimitives.AtomicPrimitivesClient
 
     constructor(
       senderPublicKey: seq<uint8>,
       recipientPublicKey: seq<uint8>,
       sharedSecret: seq<uint8>,
       keyringVersion: seq<uint8>,
       curveSpec: PrimitiveTypes.ECDHCurveSpec,
-      crypto: Primitives.AtomicPrimitivesClient
+      crypto: AtomicPrimitives.AtomicPrimitivesClient
     )
       requires crypto.ValidState()
       ensures
@@ -228,12 +228,12 @@ module {:options "/functionSyntax:4" } EcdhEdkWrapping {
   {
     const sharedSecret: seq<uint8>
     const fixedInfo: seq<uint8>
-    const crypto: Primitives.AtomicPrimitivesClient
+    const crypto: AtomicPrimitives.AtomicPrimitivesClient
 
     constructor(
       sharedSecret: seq<uint8>,
       fixedInfo: seq<uint8>,
-      crypto: Primitives.AtomicPrimitivesClient
+      crypto: AtomicPrimitives.AtomicPrimitivesClient
     )
       requires crypto.ValidState()
       ensures
@@ -316,12 +316,12 @@ module {:options "/functionSyntax:4" } EcdhEdkWrapping {
   {
     const sharedSecret: seq<uint8>
     const fixedInfo: seq<uint8>
-    const crypto: Primitives.AtomicPrimitivesClient
+    const crypto: AtomicPrimitives.AtomicPrimitivesClient
 
     constructor(
       sharedSecret: seq<uint8>,
       fixedInfo: seq<uint8>,
-      crypto: Primitives.AtomicPrimitivesClient
+      crypto: AtomicPrimitives.AtomicPrimitivesClient
     )
       requires crypto.ValidState()
       ensures
@@ -461,7 +461,7 @@ module {:options "/functionSyntax:4" } EcdhEdkWrapping {
     sharedSecret: seq<uint8>,
     fixedInfo: seq<uint8>,
     salt: seq<uint8>,
-    crypto: Primitives.AtomicPrimitivesClient
+    crypto: AtomicPrimitives.AtomicPrimitivesClient
   ) returns (res :Result<seq<uint8>, Types.Error>)
     requires crypto.ValidState()
     modifies crypto.Modifies

AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/KeyWrapping/EdkWrapping.dfy

@@ -20,7 +20,7 @@ module EdkWrapping {
   import opened IntermediateKeyWrapping
   import Crypto = AwsCryptographyPrimitivesTypes
   import Types = AwsCryptographyMaterialProvidersTypes
-  import Aws.Cryptography.Primitives
+  import AtomicPrimitives
   import Materials
   import AlgorithmSuites
 

AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/KeyWrapping/IntermediateKeyWrapping.dfy

@@ -15,7 +15,7 @@ module IntermediateKeyWrapping {
   import opened AlgorithmSuites
   import Crypto = AwsCryptographyPrimitivesTypes
   import Types = AwsCryptographyMaterialProvidersTypes
-  import Aws.Cryptography.Primitives
+  import AtomicPrimitives
   import Materials
   import UTF8
   import HKDF
@@ -74,11 +74,11 @@ module IntermediateKeyWrapping {
           [])
 
   {
-    var maybeCrypto := Primitives.AtomicPrimitives();
+    var maybeCrypto := AtomicPrimitives.AtomicPrimitives();
     var cryptoPrimitivesX : Crypto.IAwsCryptographicPrimitivesClient :- maybeCrypto
     .MapFailure(e => Types.AwsCryptographyPrimitives(e));
-    assert cryptoPrimitivesX is Primitives.AtomicPrimitivesClient;
-    var cryptoPrimitives := cryptoPrimitivesX as Primitives.AtomicPrimitivesClient;
+    assert cryptoPrimitivesX is AtomicPrimitives.AtomicPrimitivesClient;
+    var cryptoPrimitives := cryptoPrimitivesX as AtomicPrimitives.AtomicPrimitivesClient;
     // Deserialize the Intermediate-Wrapped material
     var deserializedWrapped :- DeserializeIntermediateWrappedMaterial(wrappedMaterial, algorithmSuite);
     var DeserializedIntermediateWrappedMaterial(encryptedPdk, providerWrappedIkm) := deserializedWrapped;
@@ -168,12 +168,12 @@ module IntermediateKeyWrapping {
         && |maybeIntermediateWrappedMat.value.encryptedPdk| ==
            (AlgorithmSuites.GetEncryptKeyLength(algorithmSuite) + AlgorithmSuites.GetEncryptTagLength(algorithmSuite)) as nat
   {
-    var maybeCrypto := Primitives.AtomicPrimitives();
+    var maybeCrypto := AtomicPrimitives.AtomicPrimitives();
     var cryptoPrimitivesX : Crypto.IAwsCryptographicPrimitivesClient :- maybeCrypto
     .MapFailure(e => Types.AwsCryptographyPrimitives(e));
 
-    assert cryptoPrimitivesX is Primitives.AtomicPrimitivesClient;
-    var cryptoPrimitives := cryptoPrimitivesX as Primitives.AtomicPrimitivesClient;
+    assert cryptoPrimitivesX is AtomicPrimitives.AtomicPrimitivesClient;
+    var cryptoPrimitives := cryptoPrimitivesX as AtomicPrimitives.AtomicPrimitivesClient;
 
 
     // Use the provider to get the intermediate key material, and wrapped intermediate key material
@@ -252,7 +252,7 @@ module IntermediateKeyWrapping {
                                        wrapInfo := res.value.wrapInfo)),
                                    [])
   {
-    var maybeCrypto := Primitives.AtomicPrimitives();
+    var maybeCrypto := AtomicPrimitives.AtomicPrimitives();
     var cryptoPrimitives :- maybeCrypto
     .MapFailure(e => Types.AwsCryptographyPrimitives(e));
 
@@ -305,7 +305,7 @@ module IntermediateKeyWrapping {
     intermediateMaterial: seq<uint8>,
     algorithmSuite: Types.AlgorithmSuiteInfo,
     encryptionContext: Types.EncryptionContext,
-    cryptoPrimitives: Primitives.AtomicPrimitivesClient
+    cryptoPrimitives: AtomicPrimitives.AtomicPrimitivesClient
   )
     returns (res: Result<PdkEncryptionAndSymmetricSigningKeys, Types.Error>)
     requires cryptoPrimitives.ValidState()

AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/KeyWrapping/MaterialWrapping.dfy

@@ -13,7 +13,7 @@ module MaterialWrapping {
   import opened Actions
   import opened Wrappers
   import Types = AwsCryptographyMaterialProvidersTypes
-  import Aws.Cryptography.Primitives
+  import AtomicPrimitives
   import Materials
   import AlgorithmSuites
 

AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsEcdhKeyring.dfy

@@ -38,7 +38,7 @@ module {:options "/functionSyntax:4" } AwsKmsEcdhKeyring {
   import MaterialWrapping
   import EcdhEdkWrapping
   import ErrorMessages
-  import Aws.Cryptography.Primitives
+  import AtomicPrimitives
   import CanonicalEncryptionContext
 
   const AWS_KMS_ECDH_KEYRING_VERSION := RawECDHKeyring.RAW_ECDH_KEYRING_VERSION
@@ -58,7 +58,7 @@ module {:options "/functionSyntax:4" } AwsKmsEcdhKeyring {
     const keyAgreementScheme: Types.KmsEcdhStaticConfigurations
     const curveSpec: PrimitiveTypes.ECDHCurveSpec
     const grantTokens: KMS.GrantTokenList
-    const cryptoPrimitives: Primitives.AtomicPrimitivesClient
+    const cryptoPrimitives: AtomicPrimitives.AtomicPrimitivesClient
 
     ghost predicate ValidState()
       ensures ValidState() ==> History in Modifies
@@ -95,7 +95,7 @@ module {:options "/functionSyntax:4" } AwsKmsEcdhKeyring {
       recipientPublicKey: KMS.PublicKeyType,
       compressedSenderPublicKey: Option<seq<uint8>>,
       compressedRecipientPublicKey: seq<uint8>,
-      cryptoPrimitives : Primitives.AtomicPrimitivesClient
+      cryptoPrimitives : AtomicPrimitives.AtomicPrimitivesClient
     )
       requires client.ValidState()
       requires cryptoPrimitives.ValidState()
@@ -438,7 +438,7 @@ module {:options "/functionSyntax:4" } AwsKmsEcdhKeyring {
       Types.Error>
   {
     const materials: Materials.DecryptionMaterialsPendingPlaintextDataKey
-    const cryptoPrimitives: Primitives.AtomicPrimitivesClient
+    const cryptoPrimitives: AtomicPrimitives.AtomicPrimitivesClient
     const recipientPublicKey: seq<uint8>
     const client: KMS.IKMSClient
     const grantTokens: KMS.GrantTokenList
@@ -447,7 +447,7 @@ module {:options "/functionSyntax:4" } AwsKmsEcdhKeyring {
 
     constructor(
       materials: Materials.DecryptionMaterialsPendingPlaintextDataKey,
-      cryptoPrimitives: Primitives.AtomicPrimitivesClient,
+      cryptoPrimitives: AtomicPrimitives.AtomicPrimitivesClient,
       recipientPublicKey: seq<uint8>,
       client: KMS.IKMSClient,
       grantTokens: KMS.GrantTokenList,

AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsHierarchicalKeyring.dfy

@@ -50,7 +50,7 @@ module AwsKmsHierarchicalKeyring {
   import HKDF
   import HMAC
   import opened AESEncryption
-  import Aws.Cryptography.Primitives
+  import AtomicPrimitives
   import ErrorMessages
 
   const BRANCH_KEY_STORE_GSI := "Active-Keys"
@@ -127,7 +127,7 @@ module AwsKmsHierarchicalKeyring {
     const branchKeyIdSupplier: Option<Types.IBranchKeyIdSupplier>
     const keyStore: KeyStore.IKeyStoreClient
     const ttlSeconds: Types.PositiveLong
-    const cryptoPrimitives: Primitives.AtomicPrimitivesClient
+    const cryptoPrimitives: AtomicPrimitives.AtomicPrimitivesClient
     const cache: Types.ICryptographicMaterialsCache
 
     predicate ValidState()
@@ -163,7 +163,7 @@ module AwsKmsHierarchicalKeyring {
       ttlSeconds: Types.PositiveLong,
 
       cmc: Types.ICryptographicMaterialsCache,
-      cryptoPrimitives : Primitives.AtomicPrimitivesClient
+      cryptoPrimitives : AtomicPrimitives.AtomicPrimitivesClient
     )
       requires ttlSeconds >= 0
       requires keyStore.ValidState() && cryptoPrimitives.ValidState()
@@ -384,7 +384,7 @@ module AwsKmsHierarchicalKeyring {
     method GetActiveCacheId(
       branchKeyId: string,
       branchKeyIdUtf8: seq<uint8>,
-      cryptoPrimitives: Primitives.AtomicPrimitivesClient
+      cryptoPrimitives: AtomicPrimitives.AtomicPrimitivesClient
     )
       returns (cacheId: Result<seq<uint8>, Types.Error>)
 
@@ -490,7 +490,7 @@ module AwsKmsHierarchicalKeyring {
     branchKey: seq<uint8>,
     salt: seq<uint8>,
     purpose: Option<seq<uint8>>,
-    cryptoPrimitives: Primitives.AtomicPrimitivesClient
+    cryptoPrimitives: AtomicPrimitives.AtomicPrimitivesClient
   )
     returns (output: Result<seq<uint8>, Types.Error>)
 
@@ -605,15 +605,15 @@ module AwsKmsHierarchicalKeyring {
   {
     const materials: Materials.DecryptionMaterialsPendingPlaintextDataKey
     const keyStore: KeyStore.IKeyStoreClient
-    const cryptoPrimitives: Primitives.AtomicPrimitivesClient
+    const cryptoPrimitives: AtomicPrimitives.AtomicPrimitivesClient
     const branchKeyId: string
     const ttlSeconds: Types.PositiveLong
     const cache: Types.ICryptographicMaterialsCache
 
     constructor(
       materials: Materials.DecryptionMaterialsPendingPlaintextDataKey,
       keyStore: KeyStore.IKeyStoreClient,
-      cryptoPrimitives: Primitives.AtomicPrimitivesClient,
+      cryptoPrimitives: AtomicPrimitives.AtomicPrimitivesClient,
       branchKeyId: string,
       ttlSeconds: Types.PositiveLong,
       cache: Types.ICryptographicMaterialsCache
@@ -697,11 +697,11 @@ module AwsKmsHierarchicalKeyring {
 
       // We need to create a new client here so that we can reason about the state of the client
       // down the line. This is ok because the only state tracked is the client's history.
-      var maybeCrypto := Primitives.AtomicPrimitives();
+      var maybeCrypto := AtomicPrimitives.AtomicPrimitives();
       var cryptoPrimitivesX : Crypto.IAwsCryptographicPrimitivesClient :- maybeCrypto
       .MapFailure(e => Types.AwsCryptographyPrimitives(e));
-      assert cryptoPrimitivesX is Primitives.AtomicPrimitivesClient;
-      var cryptoPrimitives := cryptoPrimitivesX as Primitives.AtomicPrimitivesClient;
+      assert cryptoPrimitivesX is AtomicPrimitives.AtomicPrimitivesClient;
+      var cryptoPrimitives := cryptoPrimitivesX as AtomicPrimitives.AtomicPrimitivesClient;
 
       var kmsHierarchyUnwrap := new KmsHierarchyUnwrapKeyMaterial(
         branchKey,
@@ -725,7 +725,7 @@ module AwsKmsHierarchicalKeyring {
     method GetVersionCacheId(
       branchKeyIdUtf8: seq<uint8>, // The branch key as Bytes
       branchKeyVersion: string,
-      cryptoPrimitives: Primitives.AtomicPrimitivesClient
+      cryptoPrimitives: AtomicPrimitives.AtomicPrimitivesClient
     )
       returns (cacheId: Result<seq<uint8>, Types.Error>)
       ensures cacheId.Success? ==> |cacheId.value| == 32
@@ -824,13 +824,13 @@ module AwsKmsHierarchicalKeyring {
     const branchKey: seq<uint8>
     const branchKeyIdUtf8 : UTF8.ValidUTF8Bytes
     const branchKeyVersionAsBytes: seq<uint8>
-    const crypto: Primitives.AtomicPrimitivesClient
+    const crypto: AtomicPrimitives.AtomicPrimitivesClient
 
     constructor(
       branchKey: seq<uint8>,
       branchKeyIdUtf8: UTF8.ValidUTF8Bytes,
       branchKeyVersionAsBytes: seq<uint8>,
-      crypto: Primitives.AtomicPrimitivesClient
+      crypto: AtomicPrimitives.AtomicPrimitivesClient
     )
       requires crypto.ValidState()
       ensures
@@ -963,13 +963,13 @@ module AwsKmsHierarchicalKeyring {
     const branchKey: seq<uint8>
     const branchKeyIdUtf8 : UTF8.ValidUTF8Bytes
     const branchKeyVersionAsBytes: seq<uint8>
-    const crypto: Primitives.AtomicPrimitivesClient
+    const crypto: AtomicPrimitives.AtomicPrimitivesClient
 
     constructor(
       branchKey: seq<uint8>,
       branchKeyIdUtf8 : UTF8.ValidUTF8Bytes,
       branchKeyVersionAsBytes: seq<uint8>,
-      crypto: Primitives.AtomicPrimitivesClient
+      crypto: AtomicPrimitives.AtomicPrimitivesClient
     )
       requires crypto.ValidState()
       ensures
@@ -1053,13 +1053,13 @@ module AwsKmsHierarchicalKeyring {
     const branchKey: seq<uint8>
     const branchKeyIdUtf8 : UTF8.ValidUTF8Bytes
     const branchKeyVersionAsBytes: seq<uint8>
-    const crypto: Primitives.AtomicPrimitivesClient
+    const crypto: AtomicPrimitives.AtomicPrimitivesClient
 
     constructor(
       branchKey: seq<uint8>,
       branchKeyIdUtf8 : UTF8.ValidUTF8Bytes,
       branchKeyVersionAsBytes: seq<uint8>,
-      crypto: Primitives.AtomicPrimitivesClient
+      crypto: AtomicPrimitives.AtomicPrimitivesClient
     )
       requires crypto.ValidState()
       ensures