Skip to content

Commit b9333fb

Browse files
authored
fix(SearchableEncryption): respect CMC contract (#1434)
1 parent 8931e27 commit b9333fb

File tree

1 file changed

+10
-1
lines changed

1 file changed

+10
-1
lines changed

DynamoDbEncryption/dafny/DynamoDbEncryption/src/SearchInfo.dfy

+10-1
Original file line numberDiff line numberDiff line change
@@ -248,6 +248,11 @@ module SearchableEncryptionInfo {
248248
assume {:axiom} cache.Modifies == {};
249249
var getCacheOutput := cache.GetCacheEntry(getCacheInput);
250250

251+
// If error is not EntryDoesNotExist, return failure
252+
if (getCacheOutput.Failure? && !getCacheOutput.error.EntryDoesNotExist?) {
253+
return Failure(AwsCryptographyMaterialProviders(AwsCryptographyMaterialProviders:=getCacheOutput.error));
254+
}
255+
251256
if getCacheOutput.Failure? {
252257
//= specification/searchable-encryption/search-config.md#beacon-keys
253258
//# Beacon keys MUST be obtained from the configured [Beacon Key Source](#beacon-key-source).
@@ -280,7 +285,11 @@ module SearchableEncryptionInfo {
280285

281286
verifyValidStateCache(cache);
282287
assume {:axiom} cache.Modifies == {};
283-
var _ := cache.PutCacheEntry(putCacheEntryInput);
288+
289+
var putResult := cache.PutCacheEntry(putCacheEntryInput);
290+
if (putResult.Failure? && !putResult.error.EntryAlreadyExists?) {
291+
return Failure(AwsCryptographyMaterialProviders(AwsCryptographyMaterialProviders:=putResult.error));
292+
}
284293
return Success(keyMap);
285294
} else {
286295
:- Need(

0 commit comments

Comments
 (0)