Merge from main by copying the diff

For some reason some code did not got merged

Author: rishav-karanjit

DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/Index.dfy

@@ -5,7 +5,7 @@ include "DdbMiddlewareConfig.dfy"
 include "AwsCryptographyDbEncryptionSdkDynamoDbTransformsOperations.dfy"
 include "../../DynamoDbEncryption/src/ConfigToInfo.dfy"
 
-module {:extern "software.amazon.cryptography.dbencryptionsdk.dynamodb.transforms.internaldafny" } DynamoDbEncryptionTransforms 
+module {:extern "software.amazon.cryptography.dbencryptionsdk.dynamodb.transforms.internaldafny" } DynamoDbEncryptionTransforms
   refines AbstractAwsCryptographyDbEncryptionSdkDynamoDbTransformsService
 {
   import opened DdbMiddlewareConfig
@@ -135,6 +135,7 @@ module {:extern "software.amazon.cryptography.dbencryptionsdk.dynamodb.transform
              (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 {})
            )
            {:nowarn} :: o; // ignore warning for missing trigger on quantifier
 
@@ -155,10 +156,11 @@ module {:extern "software.amazon.cryptography.dbencryptionsdk.dynamodb.transform
       var tableName: string := tableNamesSeq[i];
 
       var inputConfig := config.tableEncryptionConfigs[tableName];
-      :- Need(inputConfig.logicalTableName !in allLogicalTableNames,  E("Duplicate logical table maped to multipule physical tables: " + inputConfig.logicalTableName));
+      :- Need(inputConfig.logicalTableName !in allLogicalTableNames,  E("Duplicate logical table mapped to multiple 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();