Skip to content

Commit bd47477

Browse files
lucasmcdonald3lucasmcdonald3
committed
use passing one
1 parent 44b0666 commit bd47477

File tree

8 files changed

+368
-167
lines changed

8 files changed

+368
-167
lines changed

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

Lines changed: 58 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
11
diff --git b/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryption/TypeConversion.cs a/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryption/TypeConversion.cs
2-
index aabc5433..0044c6b7 100644
2+
index aabc5433..a2a04f8c 100644
33
--- b/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryption/TypeConversion.cs
44
+++ a/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryption/TypeConversion.cs
55
@@ -7,10 +7,43 @@ namespace AWS.Cryptography.DbEncryptionSDK.DynamoDb
@@ -49,3 +49,60 @@ index aabc5433..0044c6b7 100644
4949
public static AWS.Cryptography.DbEncryptionSDK.DynamoDb.BeaconKeySource FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S15_BeaconKeySource(software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types._IBeaconKeySource value)
5050
{
5151
software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.BeaconKeySource concrete = (software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.BeaconKeySource)value;
52+
@@ -925,11 +958,6 @@ namespace AWS.Cryptography.DbEncryptionSDK.DynamoDb
53+
converted.StormTracking = FromDafny_N3_aws__N12_cryptography__N17_materialProviders__S9_CacheType__M13_StormTracking(concrete.dtor_StormTracking);
54+
return converted;
55+
}
56+
- if (value.is_Shared)
57+
- {
58+
- converted.Shared = FromDafny_N3_aws__N12_cryptography__N17_materialProviders__S9_CacheType__M6_Shared(concrete.dtor_Shared);
59+
- return converted;
60+
- }
61+
throw new System.ArgumentException("Invalid AWS.Cryptography.MaterialProviders.CacheType state");
62+
}
63+
public static software.amazon.cryptography.materialproviders.internaldafny.types._ICacheType ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S9_CacheType(AWS.Cryptography.MaterialProviders.CacheType value)
64+
@@ -954,10 +982,6 @@ namespace AWS.Cryptography.DbEncryptionSDK.DynamoDb
65+
{
66+
return software.amazon.cryptography.materialproviders.internaldafny.types.CacheType.create_StormTracking(ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S9_CacheType__M13_StormTracking(value.StormTracking));
67+
}
68+
- if (value.IsSetShared())
69+
- {
70+
- return software.amazon.cryptography.materialproviders.internaldafny.types.CacheType.create_Shared(ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S9_CacheType__M6_Shared(value.Shared));
71+
- }
72+
throw new System.ArgumentException("Invalid AWS.Cryptography.MaterialProviders.CacheType state");
73+
}
74+
public static string FromDafny_N3_com__N9_amazonaws__N8_dynamodb__S13_AttributeName(Dafny.ISequence<char> value)
75+
@@ -1130,14 +1154,6 @@ namespace AWS.Cryptography.DbEncryptionSDK.DynamoDb
76+
{
77+
return ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S18_StormTrackingCache(value);
78+
}
79+
- public static AWS.Cryptography.MaterialProviders.ICryptographicMaterialsCache FromDafny_N3_aws__N12_cryptography__N17_materialProviders__S9_CacheType__M6_Shared(software.amazon.cryptography.materialproviders.internaldafny.types.ICryptographicMaterialsCache value)
80+
- {
81+
- return FromDafny_N3_aws__N12_cryptography__N17_materialProviders__S36_CryptographicMaterialsCacheReference(value);
82+
- }
83+
- public static software.amazon.cryptography.materialproviders.internaldafny.types.ICryptographicMaterialsCache ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S9_CacheType__M6_Shared(AWS.Cryptography.MaterialProviders.ICryptographicMaterialsCache value)
84+
- {
85+
- return ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S36_CryptographicMaterialsCacheReference(value);
86+
- }
87+
public static string FromDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M1_S(Dafny.ISequence<char> value)
88+
{
89+
return FromDafny_N3_com__N9_amazonaws__N8_dynamodb__S20_StringAttributeValue(value);
90+
@@ -1308,18 +1324,6 @@ namespace AWS.Cryptography.DbEncryptionSDK.DynamoDb
91+
int? var_entryPruningTailSize = value.IsSetEntryPruningTailSize() ? value.EntryPruningTailSize : (int?)null;
92+
return new software.amazon.cryptography.materialproviders.internaldafny.types.StormTrackingCache(ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S18_StormTrackingCache__M13_entryCapacity(value.EntryCapacity), ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S18_StormTrackingCache__M20_entryPruningTailSize(var_entryPruningTailSize), ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S18_StormTrackingCache__M11_gracePeriod(value.GracePeriod), ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S18_StormTrackingCache__M13_graceInterval(value.GraceInterval), ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S18_StormTrackingCache__M6_fanOut(value.FanOut), ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S18_StormTrackingCache__M11_inFlightTTL(value.InFlightTTL), ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S18_StormTrackingCache__M10_sleepMilli(value.SleepMilli));
93+
}
94+
- public static AWS.Cryptography.MaterialProviders.ICryptographicMaterialsCache FromDafny_N3_aws__N12_cryptography__N17_materialProviders__S36_CryptographicMaterialsCacheReference(software.amazon.cryptography.materialproviders.internaldafny.types.ICryptographicMaterialsCache value)
95+
- {
96+
- // This is converting a reference type in a dependant module.
97+
- // Therefore it defers to the dependant module for conversion
98+
- return AWS.Cryptography.MaterialProviders.TypeConversion.FromDafny_N3_aws__N12_cryptography__N17_materialProviders__S36_CryptographicMaterialsCacheReference(value);
99+
- }
100+
- public static software.amazon.cryptography.materialproviders.internaldafny.types.ICryptographicMaterialsCache ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S36_CryptographicMaterialsCacheReference(AWS.Cryptography.MaterialProviders.ICryptographicMaterialsCache value)
101+
- {
102+
- // This is converting a reference type in a dependant module.
103+
- // Therefore it defers to the dependant module for conversion
104+
- return AWS.Cryptography.MaterialProviders.TypeConversion.ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S36_CryptographicMaterialsCacheReference(value);
105+
- }
106+
public static string FromDafny_N3_com__N9_amazonaws__N8_dynamodb__S20_StringAttributeValue(Dafny.ISequence<char> value)
107+
{
108+
return new string(value.Elements);

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

Lines changed: 145 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,145 @@
1+
diff --git b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/Model/AwsCryptographyDbEncryptionSdkDynamoDbTransformsTypes.dfy a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/Model/AwsCryptographyDbEncryptionSdkDynamoDbTransformsTypes.dfy
2+
index 9a8ed7f4..1ffa8b55 100644
3+
--- b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/Model/AwsCryptographyDbEncryptionSdkDynamoDbTransformsTypes.dfy
4+
+++ a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/Model/AwsCryptographyDbEncryptionSdkDynamoDbTransformsTypes.dfy
5+
@@ -759,94 +759,62 @@ 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+
+ modifies set tmps5 <- set t5 <- config.tableEncryptionConfigs.Values | true
19+
+ && t5.keyring.Some?
20+
+ :: t5.keyring.value,
21+
+ obj <- tmps5.Modifies | obj in tmps5.Modifies :: obj
22+
+ modifies set tmps6 <- set t6 <- config.tableEncryptionConfigs.Values | true
23+
+ && t6.cmm.Some?
24+
+ :: t6.cmm.value,
25+
+ obj <- tmps6.Modifies | obj in tmps6.Modifies :: obj
26+
modifies set tmps7 <- set t7 <- config.tableEncryptionConfigs.Values | true
27+
- && t7.keyring.Some?
28+
- :: t7.keyring.value,
29+
+ && t7.legacyOverride.Some?
30+
+ :: t7.legacyOverride.value.encryptor,
31+
obj <- tmps7.Modifies | obj in tmps7.Modifies :: obj
32+
modifies set tmps8 <- set t8 <- config.tableEncryptionConfigs.Values | true
33+
- && t8.cmm.Some?
34+
- :: t8.cmm.value,
35+
+ && t8.search.Some?
36+
+ , t9 <- t8.search.value.versions :: t9.keyStore,
37+
obj <- tmps8.Modifies | obj in tmps8.Modifies :: obj
38+
- modifies set tmps9 <- set t9 <- config.tableEncryptionConfigs.Values | true
39+
- && t9.legacyOverride.Some?
40+
- :: t9.legacyOverride.value.encryptor,
41+
- obj <- tmps9.Modifies | obj in tmps9.Modifies :: obj
42+
- modifies set tmps10 <- set t10 <- config.tableEncryptionConfigs.Values | true
43+
- && t10.search.Some?
44+
- , t11 <- t10.search.value.versions :: t11.keyStore,
45+
- obj <- tmps10.Modifies | obj in tmps10.Modifies :: obj
46+
- modifies set tmps12 <- set t12 <- config.tableEncryptionConfigs.Values | true
47+
- && t12.search.Some?
48+
- , t13 <- t12.search.value.versions && t13.keySource.multi?
49+
- && t13.keySource.multi.cache.Some?
50+
- && t13.keySource.multi.cache.value.Shared?
51+
- :: t13.keySource.multi.cache.value.Shared,
52+
- obj <- tmps12.Modifies | obj in tmps12.Modifies :: obj
53+
ensures res.Success? ==>
54+
&& fresh(res.value)
55+
&& fresh(res.value.Modifies
56+
- - ( set tmps14 <- set t14 <- config.tableEncryptionConfigs.Values | true
57+
- && t14.keyring.Some?
58+
- :: t14.keyring.value,
59+
- obj <- tmps14.Modifies | obj in tmps14.Modifies :: obj
60+
- ) - ( set tmps15 <- set t15 <- config.tableEncryptionConfigs.Values | true
61+
- && t15.cmm.Some?
62+
- :: t15.cmm.value,
63+
- obj <- tmps15.Modifies | obj in tmps15.Modifies :: obj
64+
- ) - ( set tmps16 <- set t16 <- config.tableEncryptionConfigs.Values | true
65+
- && t16.legacyOverride.Some?
66+
- :: t16.legacyOverride.value.encryptor,
67+
- obj <- tmps16.Modifies | obj in tmps16.Modifies :: obj
68+
- ) - ( set tmps17 <- set t17 <- config.tableEncryptionConfigs.Values | true
69+
- && t17.search.Some?
70+
- , t18 <- t17.search.value.versions :: t18.keyStore,
71+
- obj <- tmps17.Modifies | obj in tmps17.Modifies :: obj
72+
- ) - ( set tmps19 <- set t19 <- config.tableEncryptionConfigs.Values | true
73+
- && t19.search.Some?
74+
- , t20 <- t19.search.value.versions && t20.keySource.multi?
75+
- && t20.keySource.multi.cache.Some?
76+
- && t20.keySource.multi.cache.value.Shared?
77+
- :: t20.keySource.multi.cache.value.Shared,
78+
- obj <- tmps19.Modifies | obj in tmps19.Modifies :: obj
79+
+ - ( set tmps10 <- set t10 <- config.tableEncryptionConfigs.Values | true
80+
+ && t10.keyring.Some?
81+
+ :: t10.keyring.value,
82+
+ obj <- tmps10.Modifies | obj in tmps10.Modifies :: obj
83+
+ ) - ( set tmps11 <- set t11 <- config.tableEncryptionConfigs.Values | true
84+
+ && t11.cmm.Some?
85+
+ :: t11.cmm.value,
86+
+ obj <- tmps11.Modifies | obj in tmps11.Modifies :: obj
87+
+ ) - ( set tmps12 <- set t12 <- config.tableEncryptionConfigs.Values | true
88+
+ && t12.legacyOverride.Some?
89+
+ :: t12.legacyOverride.value.encryptor,
90+
+ obj <- tmps12.Modifies | obj in tmps12.Modifies :: obj
91+
+ ) - ( set tmps13 <- set t13 <- config.tableEncryptionConfigs.Values | true
92+
+ && t13.search.Some?
93+
+ , t14 <- t13.search.value.versions :: t14.keyStore,
94+
+ obj <- tmps13.Modifies | obj in tmps13.Modifies :: obj
95+
) )
96+
&& fresh(res.value.History)
97+
&& res.value.ValidState()
98+
- ensures var tmps21 := set t21 | t21 in config.tableEncryptionConfigs.Values;
99+
- forall tmp21 :: tmp21 in tmps21 ==>
100+
- tmp21.keyring.Some? ==>
101+
- tmp21.keyring.value.ValidState()
102+
- ensures var tmps22 := set t22 | t22 in config.tableEncryptionConfigs.Values;
103+
- forall tmp22 :: tmp22 in tmps22 ==>
104+
- tmp22.cmm.Some? ==>
105+
- tmp22.cmm.value.ValidState()
106+
- ensures var tmps23 := set t23 | t23 in config.tableEncryptionConfigs.Values;
107+
- forall tmp23 :: tmp23 in tmps23 ==>
108+
- tmp23.legacyOverride.Some? ==>
109+
- tmp23.legacyOverride.value.encryptor.ValidState()
110+
- ensures var tmps24 := set t24 | t24 in config.tableEncryptionConfigs.Values;
111+
- forall tmp24 :: tmp24 in tmps24 ==>
112+
- tmp24.search.Some? ==>
113+
- var tmps25 := set t25 | t25 in tmp24.search.value.versions;
114+
- forall tmp25 :: tmp25 in tmps25 ==>
115+
- tmp25.keyStore.ValidState()
116+
- ensures var tmps26 := set t26 | t26 in config.tableEncryptionConfigs.Values;
117+
- forall tmp26 :: tmp26 in tmps26 ==>
118+
- tmp26.search.Some? ==>
119+
- var tmps27 := set t27 | t27 in tmp26.search.value.versions;
120+
- forall tmp27 :: tmp27 in tmps27 ==>
121+
- tmp27.keySource.multi? ==>
122+
- tmp27.keySource.multi.cache.Some? ==>
123+
- tmp27.keySource.multi.cache.value.Shared? ==>
124+
- tmp27.keySource.multi.cache.value.Shared.ValidState()
125+
+ ensures var tmps15 := set t15 | t15 in config.tableEncryptionConfigs.Values;
126+
+ forall tmp15 :: tmp15 in tmps15 ==>
127+
+ tmp15.keyring.Some? ==>
128+
+ tmp15.keyring.value.ValidState()
129+
+ ensures var tmps16 := set t16 | t16 in config.tableEncryptionConfigs.Values;
130+
+ forall tmp16 :: tmp16 in tmps16 ==>
131+
+ tmp16.cmm.Some? ==>
132+
+ tmp16.cmm.value.ValidState()
133+
+ ensures var tmps17 := set t17 | t17 in config.tableEncryptionConfigs.Values;
134+
+ forall tmp17 :: tmp17 in tmps17 ==>
135+
+ tmp17.legacyOverride.Some? ==>
136+
+ tmp17.legacyOverride.value.encryptor.ValidState()
137+
+ ensures var tmps18 := set t18 | t18 in config.tableEncryptionConfigs.Values;
138+
+ forall tmp18 :: tmp18 in tmps18 ==>
139+
+ tmp18.search.Some? ==>
140+
+ var tmps19 := set t19 | t19 in tmp18.search.value.versions;
141+
+ forall tmp19 :: tmp19 in tmps19 ==>
142+
+ tmp19.keyStore.ValidState()
143+
144+
// Helper functions for the benefit of native code to create a Success(client) without referring to Dafny internals
145+
function method CreateSuccessOfClient(client: IDynamoDbEncryptionTransformsClient): Result<IDynamoDbEncryptionTransformsClient, Error> {

0 commit comments

Comments
 (0)