diff --git a/DynamoDbEncryption/dafny/DynamoDbItemEncryptor/src/Index.dfy b/DynamoDbEncryption/dafny/DynamoDbItemEncryptor/src/Index.dfy
index 0c8dc3566..c42bd2698 100644
--- a/DynamoDbEncryption/dafny/DynamoDbItemEncryptor/src/Index.dfy
+++ b/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 {} )
diff --git a/TestVectors/dafny/DDBEncryption/src/JsonConfig.dfy b/TestVectors/dafny/DDBEncryption/src/JsonConfig.dfy
index 1471408bc..ad3c6d49a 100644
--- a/TestVectors/dafny/DDBEncryption/src/JsonConfig.dfy
+++ b/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(
diff --git a/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy b/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy
index b8ff98b15..09a490d7d 100644
--- a/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy
+++ b/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
diff --git a/project.properties b/project.properties
index 30877786f..b4cf8f582 100644
--- a/project.properties
+++ b/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
diff --git a/submodules/MaterialProviders b/submodules/MaterialProviders
index 3e2a1654a..5f8d816df 160000
--- a/submodules/MaterialProviders
+++ b/submodules/MaterialProviders
@@ -1 +1 @@
-Subproject commit 3e2a1654a12e64fc0e76a117f6641ec761f8f241
+Subproject commit 5f8d816df1febed28bed1ba6c63cc9c826ae61a8