Skip to content

Commit c3d1741

Browse files
lucasmcdonald3lucasmcdonald3
committed
m
1 parent bf913a1 commit c3d1741

File tree

1 file changed

+72
-1
lines changed
  • DynamoDbEncryption/codegen-patches/DynamoDbEncryptionTransforms/dafny

1 file changed

+72
-1
lines changed

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

+72-1
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,78 @@
11
diff --git b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/Model/AwsCryptographyDbEncryptionSdkDynamoDbTransformsTypes.dfy a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/Model/AwsCryptographyDbEncryptionSdkDynamoDbTransformsTypes.dfy
2-
index b3a92716..85d4f302 100644
2+
index b3a92716..24f9d302 100644
33
--- b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/Model/AwsCryptographyDbEncryptionSdkDynamoDbTransformsTypes.dfy
44
+++ a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/Model/AwsCryptographyDbEncryptionSdkDynamoDbTransformsTypes.dfy
5+
@@ -759,15 +759,15 @@ abstract module AbstractAwsCryptographyDbEncryptionSdkDynamoDbTransformsService
6+
var tmps4 := set t4 | t4 in tmp3.search.value.versions;
7+
forall tmp4 :: tmp4 in tmps4 ==>
8+
tmp4.keyStore.ValidState()
9+
- requires var tmps5 := set t5 | t5 in config.tableEncryptionConfigs.Values;
10+
- forall tmp5 :: tmp5 in tmps5 ==>
11+
- tmp5.search.Some? ==>
12+
- var tmps6 := set t6 | t6 in tmp5.search.value.versions;
13+
- forall tmp6 :: tmp6 in tmps6 ==>
14+
- tmp6.keySource.multi? ==>
15+
- tmp6.keySource.multi.cache.Some? ==>
16+
- tmp6.keySource.multi.cache.value.Shared? ==>
17+
- tmp6.keySource.multi.cache.value.Shared.ValidState()
18+
+ // requires var tmps5 := set t5 | t5 in config.tableEncryptionConfigs.Values;
19+
+ // forall tmp5 :: tmp5 in tmps5 ==>
20+
+ // tmp5.search.Some? ==>
21+
+ // var tmps6 := set t6 | t6 in tmp5.search.value.versions;
22+
+ // forall tmp6 :: tmp6 in tmps6 ==>
23+
+ // tmp6.keySource.multi? ==>
24+
+ // tmp6.keySource.multi.cache.Some? ==>
25+
+ // tmp6.keySource.multi.cache.value.Shared? ==>
26+
+ // tmp6.keySource.multi.cache.value.Shared.ValidState()
27+
modifies set tmps7 <- set t7 <- config.tableEncryptionConfigs.Values | true
28+
&& t7.keyring.Some?
29+
:: t7.keyring.value,
30+
@@ -785,14 +785,14 @@ abstract module AbstractAwsCryptographyDbEncryptionSdkDynamoDbTransformsService
31+
, t11 <- t10.search.value.versions | true
32+
:: t11.keyStore,
33+
obj <- tmps10.Modifies | obj in tmps10.Modifies :: obj
34+
- modifies set tmps12 <- set t12 <- config.tableEncryptionConfigs.Values | true
35+
- && t12.search.Some?
36+
- , t13 <- t12.search.value.versions | true
37+
- && t13.keySource.multi?
38+
- && t13.keySource.multi.cache.Some?
39+
- && t13.keySource.multi.cache.value.Shared?
40+
- :: t13.keySource.multi.cache.value.Shared,
41+
- obj <- tmps12.Modifies | obj in tmps12.Modifies :: obj
42+
+ // modifies set tmps12 <- set t12 <- config.tableEncryptionConfigs.Values | true
43+
+ // && t12.search.Some?
44+
+ // , t13 <- t12.search.value.versions | true
45+
+ // && t13.keySource.multi?
46+
+ // && t13.keySource.multi.cache.Some?
47+
+ // && t13.keySource.multi.cache.value.Shared?
48+
+ // :: t13.keySource.multi.cache.value.Shared,
49+
+ // obj <- tmps12.Modifies | obj in tmps12.Modifies :: obj
50+
ensures res.Success? ==>
51+
&& fresh(res.value)
52+
&& fresh(res.value.Modifies
53+
@@ -813,14 +813,14 @@ abstract module AbstractAwsCryptographyDbEncryptionSdkDynamoDbTransformsService
54+
, t18 <- t17.search.value.versions | true
55+
:: t18.keyStore,
56+
obj <- tmps17.Modifies | obj in tmps17.Modifies :: obj
57+
- ) - ( set tmps19 <- set t19 <- config.tableEncryptionConfigs.Values | true
58+
- && t19.search.Some?
59+
- , t20 <- t19.search.value.versions | true
60+
- && t20.keySource.multi?
61+
- && t20.keySource.multi.cache.Some?
62+
- && t20.keySource.multi.cache.value.Shared?
63+
- :: t20.keySource.multi.cache.value.Shared,
64+
- obj <- tmps19.Modifies | obj in tmps19.Modifies :: obj
65+
+ // ) - ( set tmps19 <- set t19 <- config.tableEncryptionConfigs.Values | true
66+
+ // && t19.search.Some?
67+
+ // , t20 <- t19.search.value.versions | true
68+
+ // && t20.keySource.multi?
69+
+ // && t20.keySource.multi.cache.Some?
70+
+ // && t20.keySource.multi.cache.value.Shared?
71+
+ // :: t20.keySource.multi.cache.value.Shared,
72+
+ // obj <- tmps19.Modifies | obj in tmps19.Modifies :: obj
73+
) )
74+
&& fresh(res.value.History)
75+
&& res.value.ValidState()
576
@@ -842,15 +842,15 @@ abstract module AbstractAwsCryptographyDbEncryptionSdkDynamoDbTransformsService
677
var tmps25 := set t25 | t25 in tmp24.search.value.versions;
778
forall tmp25 :: tmp25 in tmps25 ==>

0 commit comments

Comments
 (0)