From 4de00d8ca6ab622812f4a7399049d8a3523d9c2b Mon Sep 17 00:00:00 2001
From: texastony <5892063+texastony@users.noreply.github.com>
Date: Fri, 11 Oct 2024 14:09:37 -0500
Subject: [PATCH] fix(SearchableEncryption): respect CMC contract

---
 .../dafny/DynamoDbEncryption/src/SearchInfo.dfy       | 11 ++++++++++-
 1 file changed, 10 insertions(+), 1 deletion(-)

diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/SearchInfo.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/SearchInfo.dfy
index 810f880dc..e1211b76a 100644
--- a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/SearchInfo.dfy
+++ b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/SearchInfo.dfy
@@ -248,6 +248,11 @@ module SearchableEncryptionInfo {
       assume {:axiom} cache.Modifies == {};
       var getCacheOutput := cache.GetCacheEntry(getCacheInput);
 
+      // If error is not EntryDoesNotExist, return failure
+      if (getCacheOutput.Failure? && !getCacheOutput.error.EntryDoesNotExist?) {
+        return Failure(AwsCryptographyMaterialProviders(AwsCryptographyMaterialProviders:=getCacheOutput.error));
+      }
+
       if getCacheOutput.Failure? {
         //= specification/searchable-encryption/search-config.md#beacon-keys
         //# Beacon keys MUST be obtained from the configured [Beacon Key Source](#beacon-key-source).
@@ -280,7 +285,11 @@ module SearchableEncryptionInfo {
 
         verifyValidStateCache(cache);
         assume {:axiom} cache.Modifies == {};
-        var _ := cache.PutCacheEntry(putCacheEntryInput);
+
+        var putResult := cache.PutCacheEntry(putCacheEntryInput);
+        if (putResult.Failure? && !putResult.error.EntryAlreadyExists?) {
+          return Failure(AwsCryptographyMaterialProviders(AwsCryptographyMaterialProviders:=putResult.error));
+        }
         return Success(keyMap);
       } else {
         :- Need(