test(SearchableEncryption): test disable shared cache via formal verificaiton

Author: texastony

DynamoDbEncryption/dafny/DynamoDbEncryption/src/ConfigToInfo.dfy

@@ -119,7 +119,21 @@ module SearchConfigToInfo {
       && config.multi.keyFieldName in outer.attributeActionsOnEncrypt
       && outer.attributeActionsOnEncrypt[config.multi.keyFieldName] == SE.ENCRYPT_AND_SIGN
       ==> output.Failure?
+    // Not in Spec, but for now, SE does not support the Shared Cache Type
+    ensures
+      && config.multi?
+      && config.multi.cache.Some?
+      && config.multi.cache.value.Shared?
+      && output.Failure?
+         // If the failure was NOT caused by booting up the MPL
+      && !output.error.AwsCryptographyMaterialProviders?
+      ==>
+        && output.error.DynamoDbEncryptionException?
+        && output.error.message == "Searchable Encryption does not support the Shared Cache type at this time."
   {
+    // TODO-FutureCleanUp : It is not-good that the MPL is initialized here;
+    // The MPL has a config object that could hold customer intent that affects behavior.
+    // Today, it does not. But tomorrow?
     var mplR := MaterialProviders.MaterialProviders();
     var mpl :- mplR.MapFailure(e => AwsCryptographyMaterialProviders(e));
 
@@ -139,7 +153,7 @@ module SearchConfigToInfo {
 
     var cache;
     if cacheType.Shared? {
-      return Failure(DynamoDbEncryptionException(message:="Searchable Encryption does not support shared caches"));
+      return Failure(DynamoDbEncryptionException(message:="Searchable Encryption does not support the Shared Cache type at this time."));
       // cache := cacheType.Shared;
     } else {
       //= specification/searchable-encryption/search-config.md#key-store-cache