[WIP] Python dbesdk changes

AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/Model/AwsCryptographyMaterialProvidersTypes.dfy

@@ -15,7 +15,7 @@ module {:extern "software.amazon.cryptography.materialproviders.internaldafny.ty
   import AwsCryptographyPrimitivesTypes
   import ComAmazonawsDynamodbTypes
   import ComAmazonawsKmsTypes
-    // Generic helpers for verification of mock/unit tests.
+  // Generic helpers for verification of mock/unit tests.
   datatype DafnyCallEvent<I, O> = DafnyCallEvent(input: I, output: O)
 
   // Begin Generated Types

AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/AlgorithmSuites.dfy

@@ -82,26 +82,26 @@ module AlgorithmSuites {
     // If there is a KDF, the output length MUST match the encrypt length
     && (a.kdf.HKDF? ==>
           && a.kdf.HKDF.outputKeyLength == a.encrypt.AES_GCM.keyLength)
-       // If there is a signature, there MUST be a KDF
+    // If there is a signature, there MUST be a KDF
     && (a.signature.ECDSA? ==> a.kdf.HKDF?)
-       // If there is commitment, the KDF MUST match
+    // If there is commitment, the KDF MUST match
     && (a.commitment.HKDF? ==>
           && a.commitment.HKDF.saltLength == 32
           && a.commitment == a.kdf)
-       // If there is a IntermediateKeyWrapping, the KDFs MUST match
+    // If there is a IntermediateKeyWrapping, the KDFs MUST match
     && (a.edkWrapping.IntermediateKeyWrapping? ==>
           && a.kdf.HKDF?
           && a.edkWrapping.IntermediateKeyWrapping.keyEncryptionKeyKdf == a.kdf
           && a.edkWrapping.IntermediateKeyWrapping.macKeyKdf == a.kdf)
-       // If there is a KDF and no commitment then salt MUST be 0
+    // If there is a KDF and no commitment then salt MUST be 0
     && (a.kdf.HKDF? && a.commitment.None? ==> a.kdf.HKDF.saltLength == 0)
-       //= aws-encryption-sdk-specification/framework/algorithm-suites.md#algorithm-suites-signature-settings
-       //= type=implication
-       //# An algorithm suite with a symmetric signature algorithm MUST use [intermediate key wrapping](#intermediate-key-wrapping).
-       //
-       // If the algorithm suite includes an symmetric signature algorithm:
-       //= aws-encryption-sdk-specification/framework/algorithm-suites.md#symmetric-signature-algorithm
-       //# - The algorithm suite MUST also use [Intermediate Key Wrapping](#intermediate-key-wrapping).
+    //= aws-encryption-sdk-specification/framework/algorithm-suites.md#algorithm-suites-signature-settings
+    //= type=implication
+    //# An algorithm suite with a symmetric signature algorithm MUST use [intermediate key wrapping](#intermediate-key-wrapping).
+    //
+    // If the algorithm suite includes an symmetric signature algorithm:
+    //= aws-encryption-sdk-specification/framework/algorithm-suites.md#symmetric-signature-algorithm
+    //# - The algorithm suite MUST also use [Intermediate Key Wrapping](#intermediate-key-wrapping).
     && (!a.symmetricSignature.None? ==>
           && a.edkWrapping.IntermediateKeyWrapping?)
   }
@@ -119,7 +119,7 @@ module AlgorithmSuites {
   {
     // Adheres to constraints for all algorithm suites
     && AlgorithmSuiteInfo?(a)
-       // All ESDK encrypt with AES_GCM
+    // All ESDK encrypt with AES_GCM
     && SupportedESDKEncrypt?(a.encrypt)
 
     // Specification for each supported ESDK Algorithm Suite

AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/CMCs/LocalCMC.dfy

@@ -344,7 +344,7 @@ module {:options "/functionSyntax:4" } LocalCMC {
       && this in InternalModifies
       && queue in InternalModifies
       && cache in InternalModifies
-                  // I want to say that `queue.Items` is somehow in InternalModifies
+      // I want to say that `queue.Items` is somehow in InternalModifies
       && (forall i <- queue.Items :: i in InternalModifies)
       && Invariant()
     }
@@ -353,15 +353,15 @@ module {:options "/functionSyntax:4" } LocalCMC {
       reads this, queue, queue.Items, cache
     {
       && queue.Invariant()
-         // The cache is a cache of Cells, these Cells MUST be unique.
-         // The actual value that the Cell contains MAY be a duplicate.
-         // See the uniqueness comment on the DoublyLinkedList.Invariant.
+      // The cache is a cache of Cells, these Cells MUST be unique.
+      // The actual value that the Cell contains MAY be a duplicate.
+      // See the uniqueness comment on the DoublyLinkedList.Invariant.
       && MutableMapIsInjective(cache)
-         // Given that cache.Values and queue.Items are unique
-         // they MUST contain exactly the same elements.
+      // Given that cache.Values and queue.Items are unique
+      // they MUST contain exactly the same elements.
       && multiset(cache.Values()) == multiset(queue.Items)
-         // To remove the tail the key associated
-         // with the tail MUST be in the cache
+      // To remove the tail the key associated
+      // with the tail MUST be in the cache
       && (forall c <- queue.Items :: c.identifier in cache.Keys() && cache.Select(c.identifier) == c)
 
       && (ValueIsSafeBecauseItIsInMemory(cache.Size()); cache.Size() as uint64 <= entryCapacity)

AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/CMCs/StormTracker.dfy

@@ -197,10 +197,10 @@ module {:options "/functionSyntax:4" }  StormTracker {
       ensures
         output ==>
           && result.expiryTime < 0x20C49BA5E353F7
-             // The + 1 comes because (now / 1000) * 1000 <= now
-             // Consider (5001 / 1000) <= 5
-             // (5001 / 1000) == 5
-             // but 5 * 1000 < 5001
+          // The + 1 comes because (now / 1000) * 1000 <= now
+          // Consider (5001 / 1000) <= 5
+          // (5001 / 1000) == 5
+          // but 5 * 1000 < 5001
           && (result.expiryTime  * 1000) - gracePeriod <= now < (result.expiryTime + 1) * 1000
     {
       // This is just showing where this constant comes from

AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/CMM.dfy

@@ -36,10 +36,10 @@ module {:options "/functionSyntax:4" } CMM {
             //# - For every key in [Required Encryption Context Keys](structures.md#required-encryption-context-keys)
             //#   there MUST be a matching key in the [Encryption Context](structures.md#encryption-context-1).
             && Materials.EncryptionMaterialsHasPlaintextDataKey(output.value.encryptionMaterials)
-               //= aws-encryption-sdk-specification/framework/cmm-interface.md#get-encryption-materials
-               //= type=implication
-               //# - The [Required Encryption Context Keys](structures.md#required-encryption-context-keys) MUST be
-               //#   a super set of the Required Encryption Context Keys in the [encryption materials request](#encryption-materials-request).
+            //= aws-encryption-sdk-specification/framework/cmm-interface.md#get-encryption-materials
+            //= type=implication
+            //# - The [Required Encryption Context Keys](structures.md#required-encryption-context-keys) MUST be
+            //#   a super set of the Required Encryption Context Keys in the [encryption materials request](#encryption-materials-request).
             && RequiredEncryptionContextKeys?(input.requiredEncryptionContextKeys, output.value.encryptionMaterials)
 
     ghost predicate DecryptMaterialsEnsuresPublicly(input: Types.DecryptMaterialsInput, output: Result<Types.DecryptMaterialsOutput, Types.Error>)
@@ -57,19 +57,19 @@ module {:options "/functionSyntax:4" } CMM {
               //# - The decryption materials returned MUST follow the specification for [decryption-materials](structures.md#decryption-materials).
               //# - The value of the plaintext data key MUST be non-NULL.
               ==> Materials.DecryptionMaterialsWithPlaintextDataKey(output.value.decryptionMaterials))
-             //= aws-encryption-sdk-specification/framework/cmm-interface.md#decrypt-materials
-             //# The CMM MUST validate the [Encryption Context](structures.md#encryption-context)
-             //# by comparing it to the customer supplied [Reproduced Encryption Context](structures.md#encryption-context)
-             //# in [decrypt materials request](#decrypt-materials-request).
-             //# For every key that exists in both [Reproduced Encryption Context](structures.md#encryption-context)
-             //# and [Encryption Context](structures.md#encryption-context),
-             //# the values MUST be equal or the operation MUST fail.
+          //= aws-encryption-sdk-specification/framework/cmm-interface.md#decrypt-materials
+          //# The CMM MUST validate the [Encryption Context](structures.md#encryption-context)
+          //# by comparing it to the customer supplied [Reproduced Encryption Context](structures.md#encryption-context)
+          //# in [decrypt materials request](#decrypt-materials-request).
+          //# For every key that exists in both [Reproduced Encryption Context](structures.md#encryption-context)
+          //# and [Encryption Context](structures.md#encryption-context),
+          //# the values MUST be equal or the operation MUST fail.
           && (output.Success? ==> ReproducedEncryptionContext?(input))
           && (!ReproducedEncryptionContext?(input) ==> output.Failure?)
-             //= aws-encryption-sdk-specification/framework/cmm-interface.md#decrypt-materials
-             //# - All key-value pairs that exist in [Reproduced Encryption Context](structures.md#encryption-context)
-             //# but do not exist in encryption context on the [decrypt materials request](#decrypt-materials-request)
-             //# SHOULD be appended to the decryption materials.
+          //= aws-encryption-sdk-specification/framework/cmm-interface.md#decrypt-materials
+          //# - All key-value pairs that exist in [Reproduced Encryption Context](structures.md#encryption-context)
+          //# but do not exist in encryption context on the [decrypt materials request](#decrypt-materials-request)
+          //# SHOULD be appended to the decryption materials.
           && (output.Success? ==> EncryptionContextComplete(input, output.value.decryptionMaterials))
   }
 

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

@@ -146,10 +146,10 @@ module DefaultCMM {
                   //# value `base64-encoded public verification key`
                   //# to the [encryption context](structures.md#encryption-context).
                   && Materials.EC_PUBLIC_KEY_FIELD in output.value.encryptionMaterials.encryptionContext
-                                                      //= aws-encryption-sdk-specification/framework/default-cmm.md#get-encryption-materials
-                                                      //= type=implication
-                                                      //# If the algorithm suite contains a [signing algorithm](algorithm-suites.md#signature-algorithm),
-                                                      //# the default CMM MUST Generate a [signing key](structures.md#signing-key).
+                  //= aws-encryption-sdk-specification/framework/default-cmm.md#get-encryption-materials
+                  //= type=implication
+                  //# If the algorithm suite contains a [signing algorithm](algorithm-suites.md#signature-algorithm),
+                  //# the default CMM MUST Generate a [signing key](structures.md#signing-key).
                   && output.value.encryptionMaterials.signingKey.Some?
                 )
 
@@ -193,25 +193,25 @@ module DefaultCMM {
         && output.Success?
         ==>
           && |keyring.History.OnEncrypt| == |old(keyring.History.OnEncrypt)| + 1
-             //= aws-encryption-sdk-specification/framework/default-cmm.md#get-encryption-materials
-             //= type=implication
-             //# On each call to Get Encryption Materials,
-             //# the default CMM MUST make a call to its [keyring's](#keyring)
-             //# [On Encrypt](keyring-interface.md#onencrypt) operation.
+          //= aws-encryption-sdk-specification/framework/default-cmm.md#get-encryption-materials
+          //= type=implication
+          //# On each call to Get Encryption Materials,
+          //# the default CMM MUST make a call to its [keyring's](#keyring)
+          //# [On Encrypt](keyring-interface.md#onencrypt) operation.
           && Seq.Last(keyring.History.OnEncrypt).output.Success?
-             //= aws-encryption-sdk-specification/framework/default-cmm.md#get-encryption-materials
-             //= type=implication
-             //# The default CMM MUST obtain the Plaintext Data Key from the
-             //# On Encrypt Response and include it in the
-             //# [encryption materials](structures.md#encryption-materials) returned.
+          //= aws-encryption-sdk-specification/framework/default-cmm.md#get-encryption-materials
+          //= type=implication
+          //# The default CMM MUST obtain the Plaintext Data Key from the
+          //# On Encrypt Response and include it in the
+          //# [encryption materials](structures.md#encryption-materials) returned.
           && Seq.Last(keyring.History.OnEncrypt).output.value.materials.plaintextDataKey
              == output.value.encryptionMaterials.plaintextDataKey
-             //= aws-encryption-sdk-specification/framework/default-cmm.md#get-encryption-materials
-             //= type=implication
-             //# The default CMM MUST obtain the
-             //# [Encrypted Data Keys](structures.md#encrypted-data-keys)
-             //# from the On Encrypt Response and include it
-             //# in the [encryption materials](structures.md#encryption-materials) returned.
+          //= aws-encryption-sdk-specification/framework/default-cmm.md#get-encryption-materials
+          //= type=implication
+          //# The default CMM MUST obtain the
+          //# [Encrypted Data Keys](structures.md#encrypted-data-keys)
+          //# from the On Encrypt Response and include it
+          //# in the [encryption materials](structures.md#encryption-materials) returned.
           && Seq.Last(keyring.History.OnEncrypt).output.value.materials.encryptedDataKeys
              == output.value.encryptionMaterials.encryptedDataKeys
 
@@ -320,11 +320,11 @@ module DefaultCMM {
       && (output.Success?
           ==>
             && Materials.DecryptionMaterialsWithPlaintextDataKey(output.value.decryptionMaterials))
-         //= aws-encryption-sdk-specification/framework/cmm-interface.md#decrypt-materials
-         //= type=implication
-         //# - All key-value pairs that exist in [Reproduced Encryption Context](structures.md#encryption-context)
-         //# but do not exist in encryption context on the [decrypt materials request](#decrypt-materials-request)
-         //# SHOULD be appended to the decryption materials.
+      //= aws-encryption-sdk-specification/framework/cmm-interface.md#decrypt-materials
+      //= type=implication
+      //# - All key-value pairs that exist in [Reproduced Encryption Context](structures.md#encryption-context)
+      //# but do not exist in encryption context on the [decrypt materials request](#decrypt-materials-request)
+      //# SHOULD be appended to the decryption materials.
       && (output.Success? ==> CMM.EncryptionContextComplete(input, output.value.decryptionMaterials))
     }
 
@@ -421,18 +421,18 @@ module DefaultCMM {
                 //# - If the decrypt materials request contains an algorithm suite,
                 //# the decryption materials returned SHOULD contain the same algorithm suite.
                 && input.algorithmSuiteId == output.value.decryptionMaterials.algorithmSuite.id
-                   //= aws-encryption-sdk-specification/framework/cmm-interface.md#decrypt-materials
-                   //= type=implication
-                   //# If the algorithm suite obtained from the decryption request contains a [signing algorithm](algorithm-suites.md#signature-algorithm),
-                   //# the decryption materials MUST include the [signature verification key](structures.md#verification-key).
+                //= aws-encryption-sdk-specification/framework/cmm-interface.md#decrypt-materials
+                //= type=implication
+                //# If the algorithm suite obtained from the decryption request contains a [signing algorithm](algorithm-suites.md#signature-algorithm),
+                //# the decryption materials MUST include the [signature verification key](structures.md#verification-key).
                 && (output.value.decryptionMaterials.algorithmSuite.signature.ECDSA? ==> output.value.decryptionMaterials.verificationKey.Some?)
 
                 && (0 < |output.value.decryptionMaterials.requiredEncryptionContextKeys| ==> input.reproducedEncryptionContext.Some?)
-                   //= aws-encryption-sdk-specification/framework/cmm-interface.md#decrypt-materials
-                   //= type=implication
-                   //# - This set MUST include all keys added to the decryption materials encryption context
-                   //# that existed in the [decrypt materials request's](#decrypt-materials-request) reproduced encryption context
-                   //# but did not exist in the [decrypt materials request's](#decrypt-materials-request) encryption context.
+                //= aws-encryption-sdk-specification/framework/cmm-interface.md#decrypt-materials
+                //= type=implication
+                //# - This set MUST include all keys added to the decryption materials encryption context
+                //# that existed in the [decrypt materials request's](#decrypt-materials-request) reproduced encryption context
+                //# but did not exist in the [decrypt materials request's](#decrypt-materials-request) encryption context.
                 && (forall key <- output.value.decryptionMaterials.requiredEncryptionContextKeys
                       ::
                         && key !in input.encryptionContext
@@ -442,17 +442,17 @@ module DefaultCMM {
         && output.Success?
         ==>
           && |keyring.History.OnDecrypt| == |old(keyring.History.OnDecrypt)| + 1
-             //= aws-encryption-sdk-specification/framework/default-cmm.md#decrypt-materials
-             //= type=implication
-             //# On each call to Decrypt Materials,
-             //# the default CMM MUST make a call to its [keyring's](#keyring)
-             //# [On Decrypt](keyring-interface.md#ondecrypt) operation.
+          //= aws-encryption-sdk-specification/framework/default-cmm.md#decrypt-materials
+          //= type=implication
+          //# On each call to Decrypt Materials,
+          //# the default CMM MUST make a call to its [keyring's](#keyring)
+          //# [On Decrypt](keyring-interface.md#ondecrypt) operation.
           && Seq.Last(keyring.History.OnDecrypt).output.Success?
-             //= aws-encryption-sdk-specification/framework/default-cmm.md#decrypt-materials
-             //= type=implication
-             //# The default CMM MUST obtain the Plaintext Data Key from
-             //# the On Decrypt response and include it in the decrypt
-             //# materials returned.
+          //= aws-encryption-sdk-specification/framework/default-cmm.md#decrypt-materials
+          //= type=implication
+          //# The default CMM MUST obtain the Plaintext Data Key from
+          //# the On Decrypt response and include it in the decrypt
+          //# materials returned.
           && Seq.Last(keyring.History.OnDecrypt).output.value.materials.plaintextDataKey
              == output.value.decryptionMaterials.plaintextDataKey
 

AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/CMMs/RequiredEncryptionContextCMM.dfy

@@ -230,11 +230,11 @@ module RequiredEncryptionContextCMM {
       && (output.Success?
           ==>
             && Materials.DecryptionMaterialsWithPlaintextDataKey(output.value.decryptionMaterials))
-         //= aws-encryption-sdk-specification/framework/cmm-interface.md#decrypt-materials
-         //= type=implication
-         //# - All key-value pairs that exist in [Reproduced Encryption Context](structures.md#encryption-context)
-         //# but do not exist in encryption context on the [decrypt materials request](#decrypt-materials-request)
-         //# SHOULD be appended to the decryption materials.
+      //= aws-encryption-sdk-specification/framework/cmm-interface.md#decrypt-materials
+      //= type=implication
+      //# - All key-value pairs that exist in [Reproduced Encryption Context](structures.md#encryption-context)
+      //# but do not exist in encryption context on the [decrypt materials request](#decrypt-materials-request)
+      //# SHOULD be appended to the decryption materials.
       && (output.Success? ==> CMM.EncryptionContextComplete(input, output.value.decryptionMaterials))
     }