Skip to content

Commit a6fca5a

Browse files
lucasmcdonald3lucasmcdonald3
committedSep 27, 2024·
m
1 parent c3d1741 commit a6fca5a

File tree

2 files changed

+34
-134
lines changed

2 files changed

+34
-134
lines changed
 

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

Lines changed: 0 additions & 100 deletions
This file was deleted.

‎DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/Model/AwsCryptographyDbEncryptionSdkDynamoDbTransformsTypes.dfy

Lines changed: 34 additions & 34 deletions
Original file line numberDiff line numberDiff line change
@@ -759,15 +759,15 @@ abstract module AbstractAwsCryptographyDbEncryptionSdkDynamoDbTransformsService
759759
var tmps4 := set t4 | t4 in tmp3.search.value.versions;
760760
forall tmp4 :: tmp4 in tmps4 ==>
761761
tmp4.keyStore.ValidState()
762-
// requires var tmps5 := set t5 | t5 in config.tableEncryptionConfigs.Values;
763-
// forall tmp5 :: tmp5 in tmps5 ==>
764-
// tmp5.search.Some? ==>
765-
// var tmps6 := set t6 | t6 in tmp5.search.value.versions;
766-
// forall tmp6 :: tmp6 in tmps6 ==>
767-
// tmp6.keySource.multi? ==>
768-
// tmp6.keySource.multi.cache.Some? ==>
769-
// tmp6.keySource.multi.cache.value.Shared? ==>
770-
// tmp6.keySource.multi.cache.value.Shared.ValidState()
762+
requires var tmps5 := set t5 | t5 in config.tableEncryptionConfigs.Values;
763+
forall tmp5 :: tmp5 in tmps5 ==>
764+
tmp5.search.Some? ==>
765+
var tmps6 := set t6 | t6 in tmp5.search.value.versions;
766+
forall tmp6 :: tmp6 in tmps6 ==>
767+
tmp6.keySource.multi? ==>
768+
tmp6.keySource.multi.cache.Some? ==>
769+
tmp6.keySource.multi.cache.value.Shared? ==>
770+
tmp6.keySource.multi.cache.value.Shared.ValidState()
771771
modifies set tmps7 <- set t7 <- config.tableEncryptionConfigs.Values | true
772772
&& t7.keyring.Some?
773773
:: t7.keyring.value,
@@ -785,14 +785,14 @@ abstract module AbstractAwsCryptographyDbEncryptionSdkDynamoDbTransformsService
785785
, t11 <- t10.search.value.versions | true
786786
:: t11.keyStore,
787787
obj <- tmps10.Modifies | obj in tmps10.Modifies :: obj
788-
// modifies set tmps12 <- set t12 <- config.tableEncryptionConfigs.Values | true
789-
// && t12.search.Some?
790-
// , t13 <- t12.search.value.versions | true
791-
// && t13.keySource.multi?
792-
// && t13.keySource.multi.cache.Some?
793-
// && t13.keySource.multi.cache.value.Shared?
794-
// :: t13.keySource.multi.cache.value.Shared,
795-
// obj <- tmps12.Modifies | obj in tmps12.Modifies :: obj
788+
modifies set tmps12 <- set t12 <- config.tableEncryptionConfigs.Values | true
789+
&& t12.search.Some?
790+
, t13 <- t12.search.value.versions | true
791+
&& t13.keySource.multi?
792+
&& t13.keySource.multi.cache.Some?
793+
&& t13.keySource.multi.cache.value.Shared?
794+
:: t13.keySource.multi.cache.value.Shared,
795+
obj <- tmps12.Modifies | obj in tmps12.Modifies :: obj
796796
ensures res.Success? ==>
797797
&& fresh(res.value)
798798
&& fresh(res.value.Modifies
@@ -813,14 +813,14 @@ abstract module AbstractAwsCryptographyDbEncryptionSdkDynamoDbTransformsService
813813
, t18 <- t17.search.value.versions | true
814814
:: t18.keyStore,
815815
obj <- tmps17.Modifies | obj in tmps17.Modifies :: obj
816-
// ) - ( set tmps19 <- set t19 <- config.tableEncryptionConfigs.Values | true
817-
// && t19.search.Some?
818-
// , t20 <- t19.search.value.versions | true
819-
// && t20.keySource.multi?
820-
// && t20.keySource.multi.cache.Some?
821-
// && t20.keySource.multi.cache.value.Shared?
822-
// :: t20.keySource.multi.cache.value.Shared,
823-
// obj <- tmps19.Modifies | obj in tmps19.Modifies :: obj
816+
) - ( set tmps19 <- set t19 <- config.tableEncryptionConfigs.Values | true
817+
&& t19.search.Some?
818+
, t20 <- t19.search.value.versions | true
819+
&& t20.keySource.multi?
820+
&& t20.keySource.multi.cache.Some?
821+
&& t20.keySource.multi.cache.value.Shared?
822+
:: t20.keySource.multi.cache.value.Shared,
823+
obj <- tmps19.Modifies | obj in tmps19.Modifies :: obj
824824
) )
825825
&& fresh(res.value.History)
826826
&& res.value.ValidState()
@@ -842,15 +842,15 @@ abstract module AbstractAwsCryptographyDbEncryptionSdkDynamoDbTransformsService
842842
var tmps25 := set t25 | t25 in tmp24.search.value.versions;
843843
forall tmp25 :: tmp25 in tmps25 ==>
844844
tmp25.keyStore.ValidState()
845-
// ensures var tmps26 := set t26 | t26 in config.tableEncryptionConfigs.Values;
846-
// forall tmp26 :: tmp26 in tmps26 ==>
847-
// tmp26.search.Some? ==>
848-
// var tmps27 := set t27 | t27 in tmp26.search.value.versions;
849-
// forall tmp27 :: tmp27 in tmps27 ==>
850-
// tmp27.keySource.multi? ==>
851-
// tmp27.keySource.multi.cache.Some? ==>
852-
// tmp27.keySource.multi.cache.value.Shared? ==>
853-
// tmp27.keySource.multi.cache.value.Shared.ValidState()
845+
ensures var tmps26 := set t26 | t26 in config.tableEncryptionConfigs.Values;
846+
forall tmp26 :: tmp26 in tmps26 ==>
847+
tmp26.search.Some? ==>
848+
var tmps27 := set t27 | t27 in tmp26.search.value.versions;
849+
forall tmp27 :: tmp27 in tmps27 ==>
850+
tmp27.keySource.multi? ==>
851+
tmp27.keySource.multi.cache.Some? ==>
852+
tmp27.keySource.multi.cache.value.Shared? ==>
853+
tmp27.keySource.multi.cache.value.Shared.ValidState()
854854

855855
// Helper functions for the benefit of native code to create a Success(client) without referring to Dafny internals
856856
function method CreateSuccessOfClient(client: IDynamoDbEncryptionTransformsClient): Result<IDynamoDbEncryptionTransformsClient, Error> {

0 commit comments

Comments
 (0)
Please sign in to comment.