Skip to content

Commit 2166afc

Browse files
seebeesseebees
committed
playing with reads
1 parent a6fca5a commit 2166afc

File tree

2 files changed

+140
-42
lines changed

2 files changed

+140
-42
lines changed

‎DynamoDbEncryption/dafny/DynamoDbEncryption/src/ConfigToInfo.dfy

+34-1
Original file line numberDiff line numberDiff line change
@@ -63,10 +63,43 @@ module SearchConfigToInfo {
6363
}
6464

6565
predicate ValidBeaconVersion(config : BeaconVersion)
66+
reads
67+
if
68+
&& config.keySource.multi?
69+
&& config.keySource.multi.cache.Some?
70+
&& config.keySource.multi.cache.value.Shared?
71+
then
72+
{config.keySource.multi.cache.value.Shared as object} + config.keySource.multi.cache.value.Shared.Modifies
73+
else {}
6674
{
67-
config.keyStore.ValidState()
75+
&& config.keyStore.ValidState()
76+
&& (
77+
&& config.keySource.multi?
78+
&& config.keySource.multi.cache.Some?
79+
&& config.keySource.multi.cache.value.Shared?
80+
==>
81+
&& config.keySource.multi.cache.value.Shared.ValidState()
82+
)
6883
}
6984
predicate ValidSearchConfig(config : Option<SearchConfig>)
85+
reads
86+
if config.Some? then
87+
set
88+
c <- config.value.versions |
89+
&& c.keySource.multi?
90+
&& c.keySource.multi.cache.Some?
91+
&& c.keySource.multi.cache.value.Shared?
92+
:: c.keySource.multi.cache.value.Shared
93+
else {},
94+
if config.Some? then
95+
set
96+
c <- config.value.versions |
97+
&& c.keySource.multi?
98+
&& c.keySource.multi.cache.Some?
99+
&& c.keySource.multi.cache.value.Shared?,
100+
o <- c.keySource.multi.cache.value.Shared.Modifies
101+
:: o
102+
else {}
70103
{
71104
if config.None? then
72105
true

‎DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/Index.dfy

+106-41
Original file line numberDiff line numberDiff line change
@@ -31,7 +31,9 @@ module
3131

3232
predicate ValidWholeSearchConfig(config : ET.DynamoDbTablesEncryptionConfig)
3333
{
34-
forall t <- config.tableEncryptionConfigs :: SearchConfigToInfo.ValidSearchConfig(config.tableEncryptionConfigs[t].search)
34+
forall t <- config.tableEncryptionConfigs
35+
::
36+
&& SearchConfigToInfo.ValidSearchConfig(config.tableEncryptionConfigs[t].search)
3537
}
3638

3739
function TheModifies(config: AwsCryptographyDbEncryptionSdkDynamoDbTypes.DynamoDbTablesEncryptionConfig) : set<object>
@@ -102,6 +104,50 @@ module
102104
&& inputConfig.sortKeyName == internalConfig.sortKeyName
103105
}
104106

107+
108+
// predicate BiteMe(
109+
// config: AwsCryptographyDbEncryptionSdkDynamoDbTypes.DynamoDbTablesEncryptionConfig
110+
// )
111+
// reads
112+
// // var tmps27 := set t27 | t27 in config.search.value.versions;
113+
114+
// set
115+
// m <- config.tableEncryptionConfigs.Values | m.search.Some?,
116+
// sv <- m.search.value.versions |
117+
// && sv.keySource.multi?
118+
// && sv.keySource.multi.cache.Some?
119+
// && sv.keySource.multi.cache.value.Shared?
120+
// ::
121+
// sv.keySource.multi.cache.value.Shared,
122+
// set
123+
// m <- config.tableEncryptionConfigs.Values | m.search.Some?,
124+
// sv <- m.search.value.versions |
125+
// && sv.keySource.multi?
126+
// && sv.keySource.multi.cache.Some?
127+
// && sv.keySource.multi.cache.value.Shared?,
128+
// o <- sv.keySource.multi.cache.value.Shared.Modifies
129+
// ::
130+
// o
131+
// // s <- m.search.value | m.search.value.keySource.multi?,
132+
// // c <- s.keySource.multi.cache | s.keySource.multi.cache.Some? && s.keySource.multi.cache.value.Shared?
133+
// // ::
134+
// // c.keySource.multi.cache.value.Shared.Modifies
135+
136+
// {
137+
// var tmps26 := set t26 | t26 in config.tableEncryptionConfigs.Values;
138+
// forall tmp26
139+
// :: tmp26 in tmps26
140+
// ==>
141+
// tmp26.search.Some? ==>
142+
// var tmps27 := set t27 | t27 in tmp26.search.value.versions;
143+
// forall tmp27
144+
// :: tmp27 in tmps27 ==>
145+
// tmp27.keySource.multi? ==>
146+
// tmp27.keySource.multi.cache.Some? ==>
147+
// tmp27.keySource.multi.cache.value.Shared? ==>
148+
// tmp27.keySource.multi.cache.value.Shared.ValidState()
149+
// }
150+
105151
method {:vcs_split_on_every_assert} DynamoDbEncryptionTransforms(config: AwsCryptographyDbEncryptionSdkDynamoDbTypes.DynamoDbTablesEncryptionConfig)
106152
returns (res: Result<DynamoDbEncryptionTransformsClient, Error>)
107153
//= specification/dynamodb-encryption-client/ddb-table-encryption-config.md#logical-table-name
@@ -115,6 +161,11 @@ module
115161
{
116162
var internalConfigs: map<string, DdbMiddlewareConfig.ValidTableConfig> := map[];
117163
assert ValidWholeSearchConfig(config);
164+
165+
// assert BiteMe(config) by {
166+
167+
// }
168+
118169
//= specification/dynamodb-encryption-client/ddb-sdk-integration.md#dynamodb-table-encryption-configs
119170
//# During initialization, this client MUST construct a
120171
//# [DynamoDb Item Encryptor](./ddb-table-encryption-config.md)
@@ -145,6 +196,8 @@ module
145196
invariant AllTableConfigsValid?(internalConfigs)
146197
invariant ValidConfig?(Config(internalConfigs))
147198

199+
// invariant BiteMe(config)
200+
148201
modifies inputConfigsModifies
149202
{
150203
var tableName: string := tableNamesSeq[i];
@@ -236,49 +289,61 @@ module
236289
assert Operations.ValidInternalConfig?(newConfig);
237290
var client := new DynamoDbEncryptionTransformsClient(newConfig);
238291

292+
// assert BiteMe(config);
293+
239294
// I'm really sorry, but I can't get the freshness to verify
240295
// and my time box has run out of time.
241296
assume {:axiom} fresh(
242-
client.Modifies
243-
- ( var tmps14 := set t14 | t14 in config.tableEncryptionConfigs.Values
244-
&& t14.keyring.Some?
245-
:: t14.keyring.value;
246-
var tmps14FlattenedModifiesSet: set<set<object>> := set t0
247-
| t0 in tmps14 :: t0.Modifies;
248-
(set tmp15ModifyEntry, tmp15Modifies |
249-
tmp15Modifies in tmps14FlattenedModifiesSet
250-
&& tmp15ModifyEntry in tmp15Modifies
251-
:: tmp15ModifyEntry)
252-
) - ( var tmps16 := set t16 | t16 in config.tableEncryptionConfigs.Values
253-
&& t16.cmm.Some?
254-
:: t16.cmm.value;
255-
var tmps16FlattenedModifiesSet: set<set<object>> := set t0
256-
| t0 in tmps16 :: t0.Modifies;
257-
(set tmp17ModifyEntry, tmp17Modifies |
258-
tmp17Modifies in tmps16FlattenedModifiesSet
259-
&& tmp17ModifyEntry in tmp17Modifies
260-
:: tmp17ModifyEntry)
261-
) - ( var tmps18 := set t18 | t18 in config.tableEncryptionConfigs.Values
262-
&& t18.legacyOverride.Some?
263-
:: t18.legacyOverride.value.encryptor;
264-
var tmps18FlattenedModifiesSet: set<set<object>> := set t0
265-
| t0 in tmps18 :: t0.Modifies;
266-
(set tmp19ModifyEntry, tmp19Modifies |
267-
tmp19Modifies in tmps18FlattenedModifiesSet
268-
&& tmp19ModifyEntry in tmp19Modifies
269-
:: tmp19ModifyEntry)
270-
) - ( var tmps20 := set t20 | t20 in config.tableEncryptionConfigs.Values
271-
&& t20.search.Some?
272-
:: set t21 | t21 in t20.search.value.versions :: t21.keyStore;
273-
var tmps20FlattenedModifiesSet: set<set<object>> := set t0
274-
, t1 | t0 in tmps20 && t1 in t0 :: t1.Modifies;
275-
(set tmp22ModifyEntry, tmp22Modifies |
276-
tmp22Modifies in tmps20FlattenedModifiesSet
277-
&& tmp22ModifyEntry in tmp22Modifies
278-
:: tmp22ModifyEntry)
279-
) );
280-
281-
return Success(client);
297+
client.Modifies
298+
- ( var tmps14 := set t14 | t14 in config.tableEncryptionConfigs.Values
299+
&& t14.keyring.Some?
300+
:: t14.keyring.value;
301+
var tmps14FlattenedModifiesSet: set<set<object>> := set t0
302+
| t0 in tmps14 :: t0.Modifies;
303+
(set tmp15ModifyEntry, tmp15Modifies |
304+
tmp15Modifies in tmps14FlattenedModifiesSet
305+
&& tmp15ModifyEntry in tmp15Modifies
306+
:: tmp15ModifyEntry)
307+
) - ( var tmps16 := set t16 | t16 in config.tableEncryptionConfigs.Values
308+
&& t16.cmm.Some?
309+
:: t16.cmm.value;
310+
var tmps16FlattenedModifiesSet: set<set<object>> := set t0
311+
| t0 in tmps16 :: t0.Modifies;
312+
(set tmp17ModifyEntry, tmp17Modifies |
313+
tmp17Modifies in tmps16FlattenedModifiesSet
314+
&& tmp17ModifyEntry in tmp17Modifies
315+
:: tmp17ModifyEntry)
316+
) - ( var tmps18 := set t18 | t18 in config.tableEncryptionConfigs.Values
317+
&& t18.legacyOverride.Some?
318+
:: t18.legacyOverride.value.encryptor;
319+
var tmps18FlattenedModifiesSet: set<set<object>> := set t0
320+
| t0 in tmps18 :: t0.Modifies;
321+
(set tmp19ModifyEntry, tmp19Modifies |
322+
tmp19Modifies in tmps18FlattenedModifiesSet
323+
&& tmp19ModifyEntry in tmp19Modifies
324+
:: tmp19ModifyEntry)
325+
) - ( var tmps20 := set t20 | t20 in config.tableEncryptionConfigs.Values
326+
&& t20.search.Some?
327+
:: set t21 | t21 in t20.search.value.versions :: t21.keyStore;
328+
var tmps20FlattenedModifiesSet: set<set<object>> := set t0
329+
, t1 | t0 in tmps20 && t1 in t0 :: t1.Modifies;
330+
(set tmp22ModifyEntry, tmp22Modifies |
331+
tmp22Modifies in tmps20FlattenedModifiesSet
332+
&& tmp22ModifyEntry in tmp22Modifies
333+
:: tmp22ModifyEntry)
334+
) );
335+
336+
res := Success(client);
337+
338+
// var tmps26 := set t26 | t26 in config.tableEncryptionConfigs.Values;
339+
// assert forall tmp26 :: tmp26 in tmps26 ==>
340+
// tmp26.search.Some? ==>
341+
// var tmps27 := set t27 | t27 in tmp26.search.value.versions;
342+
// forall tmp27 :: tmp27 in tmps27 ==>
343+
// tmp27.keySource.multi? ==>
344+
// tmp27.keySource.multi.cache.Some? ==>
345+
// tmp27.keySource.multi.cache.value.Shared? ==>
346+
// tmp27.keySource.multi.cache.value.Shared.ValidState();
282347
}
283348

284349
// lemma ConstructionOK(config : DdbMiddlewareConfig.Config)

0 commit comments

Comments
 (0)