1
1
diff --git b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/Model/AwsCryptographyDbEncryptionSdkDynamoDbTransformsTypes.dfy a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/Model/AwsCryptographyDbEncryptionSdkDynamoDbTransformsTypes.dfy
2
- index b3a92716..6a6abcfc 100644
2
+ index b3a92716..85d4f302 100644
3
3
--- b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/Model/AwsCryptographyDbEncryptionSdkDynamoDbTransformsTypes.dfy
4
4
+++ a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/Model/AwsCryptographyDbEncryptionSdkDynamoDbTransformsTypes.dfy
5
5
@@ -842,15 +842,15 @@ abstract module AbstractAwsCryptographyDbEncryptionSdkDynamoDbTransformsService
@@ -15,15 +15,15 @@ index b3a92716..6a6abcfc 100644
15
15
- tmp27.keySource.multi.cache.Some? ==>
16
16
- tmp27.keySource.multi.cache.value.Shared? ==>
17
17
- tmp27.keySource.multi.cache.value.Shared.ValidState()
18
- + // ensures var tmps26 := set t26 | t26 in config.tableEncryptionConfigs.Values;
19
- + // forall tmp26 :: tmp26 in tmps26 ==>
20
- + // tmp26.search.Some? ==>
21
- + // var tmps27 := set t27 | t27 in tmp26.search.value.versions;
22
- + // forall tmp27 :: tmp27 in tmps27 ==>
23
- + // tmp27.keySource.multi? ==>
24
- + // tmp27.keySource.multi.cache.Some? ==>
25
- + // tmp27.keySource.multi.cache.value.Shared? ==>
26
- + // tmp27.keySource.multi.cache.value.Shared.ValidState()
18
+ + // ensures var tmps26 := set t26 | t26 in config.tableEncryptionConfigs.Values;
19
+ + // forall tmp26 :: tmp26 in tmps26 ==>
20
+ + // tmp26.search.Some? ==>
21
+ + // var tmps27 := set t27 | t27 in tmp26.search.value.versions;
22
+ + // forall tmp27 :: tmp27 in tmps27 ==>
23
+ + // tmp27.keySource.multi? ==>
24
+ + // tmp27.keySource.multi.cache.Some? ==>
25
+ + // tmp27.keySource.multi.cache.value.Shared? ==>
26
+ + // tmp27.keySource.multi.cache.value.Shared.ValidState()
27
27
28
28
// Helper functions for the benefit of native code to create a Success(client) without referring to Dafny internals
29
29
function method CreateSuccessOfClient(client: IDynamoDbEncryptionTransformsClient): Result<IDynamoDbEncryptionTransformsClient, Error> {
0 commit comments