diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/QueryTransform.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/QueryTransform.dfy
index 6eefe7fa2..e9d601f94 100644
--- a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/QueryTransform.dfy
+++ b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/QueryTransform.dfy
@@ -92,16 +92,6 @@ module QueryTransform {
       var decryptRes := tableConfig.itemEncryptor.DecryptItem(decryptInput);
       var decrypted :- MapError(decryptRes);
 
-      // If the decrypted result was plaintext, i.e. has no parsedHeader
-      // then this is expected IFF the table config allows plaintext read
-      assert decrypted.parsedHeader.None? ==>
-          && EncOps.IsPlaintextItem(encryptedItems[x])
-          && !tableConfig.plaintextOverride.FORBID_PLAINTEXT_WRITE_FORBID_PLAINTEXT_READ?
-          && (
-               || tableConfig.plaintextOverride.FORBID_PLAINTEXT_WRITE_ALLOW_PLAINTEXT_READ?
-               || tableConfig.plaintextOverride.FORCE_PLAINTEXT_WRITE_ALLOW_PLAINTEXT_READ?
-             );
-
       if keyId.KeyId? && decrypted.parsedHeader.Some? {
         :- Need(|decrypted.parsedHeader.value.encryptedDataKeys| == 1, E("Query result has more than one Encrypted Data Key"));
         if decrypted.parsedHeader.value.encryptedDataKeys[0].keyProviderInfo == keyIdUtf8 {
diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/ScanTransform.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/ScanTransform.dfy
index 034cd7943..e412e5121 100644
--- a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/ScanTransform.dfy
+++ b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/ScanTransform.dfy
@@ -90,16 +90,6 @@ module ScanTransform {
       var decryptRes := tableConfig.itemEncryptor.DecryptItem(decryptInput);
       var decrypted :- MapError(decryptRes);
 
-      // If the decrypted result was plaintext, i.e. has no parsedHeader
-      // then this is expected IFF the table config allows plaintext read
-      assert decrypted.parsedHeader.None? ==>
-          && EncOps.IsPlaintextItem(encryptedItems[x])
-          && !tableConfig.plaintextOverride.FORBID_PLAINTEXT_WRITE_FORBID_PLAINTEXT_READ?
-          && (
-               || tableConfig.plaintextOverride.FORBID_PLAINTEXT_WRITE_ALLOW_PLAINTEXT_READ?
-               || tableConfig.plaintextOverride.FORCE_PLAINTEXT_WRITE_ALLOW_PLAINTEXT_READ?
-             );
-
       if keyId.KeyId? && decrypted.parsedHeader.Some? {
         :- Need(|decrypted.parsedHeader.value.encryptedDataKeys| == 1, E("Scan result has more than one Encrypted Data Key"));
         if decrypted.parsedHeader.value.encryptedDataKeys[0].keyProviderInfo == keyIdUtf8 {
diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/test/TestFixtures.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/test/TestFixtures.dfy
index 2667e361c..bb6633666 100644
--- a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/test/TestFixtures.dfy
+++ b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/test/TestFixtures.dfy
@@ -243,6 +243,7 @@ module TestFixtures {
     ensures fresh(encryption)
     ensures fresh(encryption.Modifies)
   {
+    expect sortKey.None? || DDB.IsValid_KeySchemaAttributeName(sortKey.value);
     var keyring := GetKmsKeyring();
     encryption :- expect DynamoDbEncryptionTransforms.DynamoDbEncryptionTransforms(
       DynamoDbTablesEncryptionConfig(
diff --git a/project.properties b/project.properties
index a20b1ec57..1a4050afc 100644
--- a/project.properties
+++ b/project.properties
@@ -1,4 +1,4 @@
-projectJavaVersion=3.6.2
+projectJavaVersion=3.6.2-SNAPSHOT
 mplDependencyJavaVersion=1.5.1
 dafnyVersion=4.2.0
 dafnyVerifyVersion=4.7.0
diff --git a/submodules/MaterialProviders b/submodules/MaterialProviders
index cdd4885cb..d51d6482e 160000
--- a/submodules/MaterialProviders
+++ b/submodules/MaterialProviders
@@ -1 +1 @@
-Subproject commit cdd4885cb22957b04167b11d8b40edbdf4301d8d
+Subproject commit d51d6482e3d8ca668111a4695d1adc0c67c3f0a3