almost fix verification

Author: RitvikKapila

DynamoDbEncryption/dafny/DynamoDbEncryption/src/ConfigToInfo.dfy

@@ -38,6 +38,7 @@ module SearchConfigToInfo {
   method Convert(outer : DynamoDbTableEncryptionConfig)
     returns (output : Result<Option<I.ValidSearchInfo>, Error>)
     requires ValidSearchConfig(outer.search)
+    requires outer.search.Some? ==> ValidSharedCache(outer.search.value.versions[0].keySource)
     ensures output.Success? && output.value.Some? ==>
               && output.value.value.ValidState()
               && fresh(output.value.value.versions[0].keySource.client)
@@ -74,6 +75,19 @@ module SearchConfigToInfo {
       forall b <- config.value.versions :: ValidBeaconVersion(b)
   }
 
+  // Valid state of the provided shared cache, if it exists
+  predicate {:opaque} ValidSharedCache(config: BeaconKeySource)
+  {
+    && (&& config.single?
+        && config.single.cache.Some?
+        && config.single.cache.value.Shared?
+        ==> && config.single.cache.value.Shared.ValidState())
+    && (&& config.multi?
+        && config.multi.cache.Some?
+        && config.multi.cache.value.Shared?
+        ==> && config.multi.cache.value.Shared.ValidState())
+  }
+
   // return true if, `keyFieldName` should be deleted from an item before writing
   function method ShouldDeleteKeyField(outer : DynamoDbTableEncryptionConfig, keyFieldName : string)
     : (ret : Result<bool, Error>)
@@ -102,6 +116,7 @@ module SearchConfigToInfo {
     returns (output : Result<I.KeySource, Error>)
     modifies client.Modifies
     requires client.ValidState()
+    requires ValidSharedCache(config)
     ensures client.ValidState()
     ensures output.Success? ==>
               && output.value.ValidState()
@@ -149,6 +164,11 @@ module SearchConfigToInfo {
     var cache;
     if cacheType.Shared? {
       cache := cacheType.Shared;
+      reveal ValidSharedCache(config, keyStore);
+
+      // This axiom is important because it is not easy to prove
+      // keyStore.Modifies !! cache.Modifies for a shared cache.
+      assume {:axiom} keyStore.Modifies !! cache.Modifies;
     } else {
       //= specification/searchable-encryption/search-config.md#key-store-cache
       //# For a Beacon Key Source a [CMC](../../submodules/MaterialProviders/aws-encryption-sdk-specification/framework/cryptographic-materials-cache.md)
@@ -196,6 +216,7 @@ module SearchConfigToInfo {
   method ConvertVersion(outer : DynamoDbTableEncryptionConfig, config : BeaconVersion)
     returns (output : Result<I.ValidBeaconVersion, Error>)
     requires ValidBeaconVersion(config)
+    requires ValidSharedCache(config.keySource)
     ensures output.Success? ==>
               && output.value.ValidState()
               && fresh(output.value.keySource.client)

DynamoDbEncryption/dafny/DynamoDbEncryption/src/SearchInfo.dfy

@@ -274,6 +274,11 @@ module SearchableEncryptionInfo {
                       && var oldPutHistory := old(cache.History.PutCacheEntry);
                       && var newPutHistory := cache.History.PutCacheEntry;
                       && |newPutHistory| == |oldPutHistory|+1
+                      && (
+                        var storeOutput := Seq.Last(newPutHistory).output;
+                        || storeOutput.Success?
+                        || storeOutput.error.EntryAlreadyExists?
+                      )
                       && var storeInput := Seq.Last(newPutHistory).input;
                       && var storeOutput := Seq.Last(newPutHistory).output;
                       //= specification/searchable-encryption/search-config.md#get-beacon-key-materials
@@ -333,14 +338,11 @@ module SearchableEncryptionInfo {
         var keyMap :- getAllKeys(stdNames, key.value);
         var beaconKeyMaterials := rawBeaconKeyMaterials.beaconKeyMaterials.(beaconKey := None, hmacKeys := Some(keyMap));
 
+        expect now < UInt.BoundedInts.INT64_MAX - cacheTTL;
           //= specification/searchable-encryption/search-config.md#get-beacon-key-materials
           //# These materials MUST be put into the associated [Key Store Cache](#key-store-cache)
           //# with an [Expiry Time](../../submodules/MaterialProviders/aws-encryption-sdk-specification/framework/cryptographic-materials-cache.md#expiry-time)
           //# equal to now + configured [cacheTTL](#cachettl).
-        :- expect Need(
-          (now as int + cacheTTL as int) < UInt.INT64_MAX_LIMIT,
-          MP.AwsCryptographicMaterialProvidersException(message := "INT64 Overflow when putting cache entry.")
-        );
         var putCacheEntryInput:= MP.PutCacheEntryInput(
           identifier := identifier,
           materials := MP.Materials.BeaconKey(beaconKeyMaterials),

DynamoDbEncryption/dafny/DynamoDbEncryption/test/BeaconTestFixtures.dfy

@@ -231,6 +231,9 @@ module BeaconTestFixtures {
     ensures output.ValidState()
     ensures version.keyStore == output.store
     ensures fresh(output.client.Modifies)
+    ensures
+      && fresh(output.cache)
+      && fresh(output.cache.Modifies)
   {
     var client :- expect Primitives.AtomicPrimitives();
 
@@ -252,6 +255,9 @@ module BeaconTestFixtures {
     ensures output.ValidState()
     ensures version.keyStore == output.store
     ensures fresh(output.client.Modifies)
+    ensures
+      && fresh(output.cache)
+      && fresh(output.cache.Modifies)
   {
     var client :- expect Primitives.AtomicPrimitives();
     var mpl :- expect MaterialProviders.MaterialProviders();

DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/Index.dfy

@@ -154,6 +154,8 @@ module
 
       assert SearchConfigToInfo.ValidSearchConfig(inputConfig.search);
       SearchInModifies(config, tableName);
+      reveal SearchConfigToInfo.ValidSharedCache();
+      assume {:axiom} inputConfig.search.Some? ==> SearchConfigToInfo.ValidSharedCache(inputConfig.search.value.versions[0].keySource);
       var searchR := SearchConfigToInfo.Convert(inputConfig);
       var search :- searchR.MapFailure(e => AwsCryptographyDbEncryptionSdkDynamoDb(e));
       assert search.None? || search.value.ValidState();