Skip to content

Commit ee868b0

Browse files
committed
format
1 parent 5ababd4 commit ee868b0

File tree

1 file changed

+12
-12
lines changed

1 file changed

+12
-12
lines changed

DynamoDbEncryption/dafny/DynamoDbEncryption/src/SearchInfo.dfy

+12-12
Original file line numberDiff line numberDiff line change
@@ -245,19 +245,19 @@ module SearchableEncryptionInfo {
245245
//# If a [cache entry](../../submodules/MaterialProviders/aws-encryption-sdk-specification/framework/cryptographic-materials-cache.md#cache-entry)
246246
//# exists, get beacon key MUST return the [entry materials](../../submodules/MaterialProviders/aws-encryption-sdk-specification/framework/cryptographic-materials-cache.md#materials).
247247
&& (cacheOutput.Success? && cacheEntryWithinLimits(
248-
creationTime := cacheOutput.value.creationTime,
249-
now := now,
250-
ttlSeconds := cacheTTL
251-
) ==>
248+
creationTime := cacheOutput.value.creationTime,
249+
now := now,
250+
ttlSeconds := cacheTTL
251+
) ==>
252252
&& cacheOutput.value.materials.BeaconKey?
253253
&& cacheOutput.value.materials.BeaconKey.hmacKeys.Some?
254254
&& output.value == cacheOutput.value.materials.BeaconKey.hmacKeys.value)
255255

256256
&& (cacheOutput.Failure? || !cacheEntryWithinLimits(
257-
creationTime := cacheOutput.value.creationTime,
258-
now := now,
259-
ttlSeconds := cacheTTL
260-
) ==>
257+
creationTime := cacheOutput.value.creationTime,
258+
now := now,
259+
ttlSeconds := cacheTTL
260+
) ==>
261261
&& var oldGetHistory := old(store.History.GetBeaconKey);
262262
&& var newGetHistory := store.History.GetBeaconKey;
263263
&& |newGetHistory| == |oldGetHistory|+1
@@ -333,10 +333,10 @@ module SearchableEncryptionInfo {
333333
var keyMap :- getAllKeys(stdNames, key.value);
334334
var beaconKeyMaterials := rawBeaconKeyMaterials.beaconKeyMaterials.(beaconKey := None, hmacKeys := Some(keyMap));
335335

336-
//= specification/searchable-encryption/search-config.md#get-beacon-key-materials
337-
//# These materials MUST be put into the associated [Key Store Cache](#key-store-cache)
338-
//# with an [Expiry Time](../../submodules/MaterialProviders/aws-encryption-sdk-specification/framework/cryptographic-materials-cache.md#expiry-time)
339-
//# equal to now + configured [cacheTTL](#cachettl).
336+
//= specification/searchable-encryption/search-config.md#get-beacon-key-materials
337+
//# These materials MUST be put into the associated [Key Store Cache](#key-store-cache)
338+
//# with an [Expiry Time](../../submodules/MaterialProviders/aws-encryption-sdk-specification/framework/cryptographic-materials-cache.md#expiry-time)
339+
//# equal to now + configured [cacheTTL](#cachettl).
340340
:- expect Need(
341341
(now as int + cacheTTL as int) < UInt.INT64_MAX_LIMIT,
342342
MP.AwsCryptographicMaterialProvidersException(message := "INT64 Overflow when putting cache entry.")

0 commit comments

Comments
 (0)