chore: Update MPL to 1.3.0 (#972)

* chore: Update MPL to 1.3.0

Author: ajewellamz

DynamoDbEncryption/dafny/DynamoDbItemEncryptor/src/Index.dfy

@@ -214,6 +214,13 @@ module
 
     var client := new DynamoDbItemEncryptorClient(internalConfig);
 
+    assert fresh(client.History);
+    assert client.Modifies == Operations.ModifiesInternalConfig(internalConfig) + {client.History};
+    assert Operations.ModifiesInternalConfig(internalConfig) ==
+           internalConfig.cmm.Modifies
+           + internalConfig.structuredEncryption.Modifies
+           + internalConfig.cmpClient.Modifies;
+
     assert fresh(client.Modifies
                  - ( if config.keyring.Some? then config.keyring.value.Modifies else {})
                  - ( if config.cmm.Some? then config.cmm.value.Modifies else {} )

TestVectors/dafny/DDBEncryption/src/JsonConfig.dfy

@@ -33,7 +33,7 @@ module {:options "-functionSyntax:4"} JsonConfig {
   import DynamoDbItemEncryptor
 
 
-  const DEFAULT_KEYS := "../../../submodules/MaterialProviders/TestVectorsAwsCryptographicMaterialProviders/dafny/TestVectorsAwsCryptographicMaterialProviders/test/keys.json"
+  const DEFAULT_KEYS : string := "../../../submodules/MaterialProviders/TestVectorsAwsCryptographicMaterialProviders/dafny/TestVectorsAwsCryptographicMaterialProviders/test/keys.json"
 
   predicate IsValidInt32(x: int)  { -0x8000_0000 <= x < 0x8000_0000}
   type ConfigName = string
@@ -298,7 +298,7 @@ module {:options "-functionSyntax:4"} JsonConfig {
 
     var keys :- expect KeyVectors.KeyVectors(
       KeyVectorsTypes.KeyVectorsConfig(
-        keyManifiestPath := DEFAULT_KEYS
+        keyManifestPath := DEFAULT_KEYS
       )
     );
     var keyDescription :-
@@ -311,7 +311,7 @@ module {:options "-functionSyntax:4"} JsonConfig {
                       .MapFailure(ParseJsonManifests.ErrorToString);
         Success(keyOut.keyDescription);
 
-    var keyring :- expect keys.CreateWappedTestVectorKeyring(KeyVectorsTypes.TestVectorKeyringInput(keyDescription := keyDescription));
+    var keyring :- expect keys.CreateWrappedTestVectorKeyring(KeyVectorsTypes.TestVectorKeyringInput(keyDescription := keyDescription));
 
     var encryptorConfig :=
         ENC.DynamoDbItemEncryptorConfig(
@@ -402,7 +402,7 @@ module {:options "-functionSyntax:4"} JsonConfig {
 
     var keys :- expect KeyVectors.KeyVectors(
       KeyVectorsTypes.KeyVectorsConfig(
-        keyManifiestPath := DEFAULT_KEYS
+        keyManifestPath := DEFAULT_KEYS
       )
     );
     var keyDescription :-
@@ -415,7 +415,7 @@ module {:options "-functionSyntax:4"} JsonConfig {
                       .MapFailure(ParseJsonManifests.ErrorToString);
         Success(keyOut.keyDescription);
 
-    var keyring :- expect keys.CreateWappedTestVectorKeyring(KeyVectorsTypes.TestVectorKeyringInput(keyDescription := keyDescription));
+    var keyring :- expect keys.CreateWrappedTestVectorKeyring(KeyVectorsTypes.TestVectorKeyringInput(keyDescription := keyDescription));
 
     var config :=
       Types.DynamoDbTableEncryptionConfig(

TestVectors/dafny/DDBEncryption/src/TestVectors.dfy

@@ -31,12 +31,8 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
   import DDB = ComAmazonawsDynamodbTypes
   import Filter = DynamoDBFilterExpr
   import SE = AwsCryptographyDbEncryptionSdkStructuredEncryptionTypes
-  import SKS = CreateStaticKeyStores
-  import KeyMaterial
   import UTF8
-  import KeyVectorsTypes = AwsCryptographyMaterialProvidersTestVectorKeysTypes
   import CMP = AwsCryptographyMaterialProvidersTypes
-  import KeyVectors
   import CreateInterceptedDDBClient
   import SortedSets
   import Seq

project.properties

@@ -1,4 +1,4 @@
 projectJavaVersion=3.3.0
-mplDependencyJavaVersion=1.2.0
+mplDependencyJavaVersion=1.3.0
 dafnyRuntimeJavaVersion=4.2.0
 smithyDafnyJavaConversionVersion=0.1