patch

Author: lucasmcdonald3

DynamoDbEncryption/codegen-patches/DynamoDbEncryptionTransforms/dafny/dafny-4.8.0.patch

@@ -0,0 +1,29 @@
+diff --git b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/Model/AwsCryptographyDbEncryptionSdkDynamoDbTransformsTypes.dfy a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/Model/AwsCryptographyDbEncryptionSdkDynamoDbTransformsTypes.dfy
+index b3a92716..6a6abcfc 100644
+--- b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/Model/AwsCryptographyDbEncryptionSdkDynamoDbTransformsTypes.dfy
++++ a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/Model/AwsCryptographyDbEncryptionSdkDynamoDbTransformsTypes.dfy
+@@ -842,15 +842,15 @@ abstract module AbstractAwsCryptographyDbEncryptionSdkDynamoDbTransformsService
+                                 var tmps25 := set t25 | t25 in tmp24.search.value.versions;
+                                 forall tmp25 :: tmp25 in tmps25 ==>
+                                                   tmp25.keyStore.ValidState()
+-    ensures var tmps26 := set t26 | t26 in config.tableEncryptionConfigs.Values;
+-            forall tmp26 :: tmp26 in tmps26 ==>
+-                              tmp26.search.Some? ==>
+-                                var tmps27 := set t27 | t27 in tmp26.search.value.versions;
+-                                forall tmp27 :: tmp27 in tmps27 ==>
+-                                                  tmp27.keySource.multi? ==>
+-                                                    tmp27.keySource.multi.cache.Some? ==>
+-                                                      tmp27.keySource.multi.cache.value.Shared? ==>
+-                                                        tmp27.keySource.multi.cache.value.Shared.ValidState()
++    // ensures var tmps26 := set t26 | t26 in config.tableEncryptionConfigs.Values;
++    //         forall tmp26 :: tmp26 in tmps26 ==> 
++    //                           tmp26.search.Some? ==>
++    //                             var tmps27 := set t27 | t27 in tmp26.search.value.versions;
++    //                             forall tmp27 :: tmp27 in tmps27 ==>
++    //                                               tmp27.keySource.multi? ==>
++    //                                                 tmp27.keySource.multi.cache.Some? ==>
++    //                                                   tmp27.keySource.multi.cache.value.Shared? ==>
++    //                                                     tmp27.keySource.multi.cache.value.Shared.ValidState()
+ 
+   // Helper functions for the benefit of native code to create a Success(client) without referring to Dafny internals
+   function method CreateSuccessOfClient(client: IDynamoDbEncryptionTransformsClient): Result<IDynamoDbEncryptionTransformsClient, Error> {