Index.dfy

Author: rishav-karanjit

DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/Index.dfy

@@ -5,9 +5,8 @@ include "DdbMiddlewareConfig.dfy"
 include "AwsCryptographyDbEncryptionSdkDynamoDbTransformsOperations.dfy"
 include "../../DynamoDbEncryption/src/ConfigToInfo.dfy"
 
-module
-  {:extern "software.amazon.cryptography.dbencryptionsdk.dynamodb.transforms.internaldafny" }
-  DynamoDbEncryptionTransforms refines AbstractAwsCryptographyDbEncryptionSdkDynamoDbTransformsService
+module {:extern "software.amazon.cryptography.dbencryptionsdk.dynamodb.transforms.internaldafny" } DynamoDbEncryptionTransforms 
+  refines AbstractAwsCryptographyDbEncryptionSdkDynamoDbTransformsService
 {
   import opened DdbMiddlewareConfig
   import opened StandardLibrary
@@ -130,7 +129,6 @@ module
              (if tableConfig.keyring.Some? then tableConfig.keyring.value.Modifies else {})
              + (if tableConfig.cmm.Some? then tableConfig.cmm.value.Modifies else {})
              + (if tableConfig.legacyOverride.Some? then tableConfig.legacyOverride.value.encryptor.Modifies else {})
-             + (if tableConfig.search.Some? then tableConfig.search.value.versions[0].keyStore.Modifies else {})
            )
       :: o;
 
@@ -151,11 +149,10 @@ module
       var tableName: string := tableNamesSeq[i];
 
       var inputConfig := config.tableEncryptionConfigs[tableName];
-      :- Need(inputConfig.logicalTableName !in allLogicalTableNames,  E("Duplicate logical table mapped to multiple physical tables: " + inputConfig.logicalTableName));
+      :- Need(inputConfig.logicalTableName !in allLogicalTableNames,  E("Duplicate logical table maped to multipule physical tables: " + inputConfig.logicalTableName));
 
       assert SearchConfigToInfo.ValidSearchConfig(inputConfig.search);
       SearchInModifies(config, tableName);
-      reveal SearchConfigToInfo.ValidSharedCache();
       var searchR := SearchConfigToInfo.Convert(inputConfig);
       var search :- searchR.MapFailure(e => AwsCryptographyDbEncryptionSdkDynamoDb(e));
       assert search.None? || search.value.ValidState();

DynamoDbEncryption/dafny/StructuredEncryption/src/Index.dfy

@@ -3,9 +3,8 @@
 
 include "AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations.dfy"
 
-module
-  {:extern "software.amazon.cryptography.dbencryptionsdk.structuredencryption.internaldafny" }
-  StructuredEncryption refines AbstractAwsCryptographyDbEncryptionSdkStructuredEncryptionService
+module {:extern "software.amazon.cryptography.dbencryptionsdk.structuredencryption.internaldafny" } StructuredEncryption 
+  refines AbstractAwsCryptographyDbEncryptionSdkStructuredEncryptionService
 {
 
   import Operations = AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations