@@ -141,6 +141,29 @@ module BeaconTestFixtures {
141
141
return store;
142
142
}
143
143
144
+ method GetMultiKeyStore () returns (output : SI. ValidStore)
145
+ ensures fresh (output. Modifies)
146
+ {
147
+ var kmsClient :- expect KMS. KMSClient ();
148
+ var ddbClient :- expect DDBC. DynamoDBClient ();
149
+ var kmsConfig := KTypes. KMSConfiguration. kmsKeyArn (
150
+ "arn:aws :kms :us -west-2:370957321024 :key /9d989aa2-2f9c-438c-a745-cc57d3ad0126"
151
+ );
152
+ var keyStoreConfig := KTypes. KeyStoreConfig (
153
+ id := None,
154
+ kmsConfiguration := kmsConfig,
155
+ logicalKeyStoreName := "KeyStoreDdbTable",
156
+ grantTokens := None,
157
+ ddbTableName := "KeyStoreDdbTable",
158
+ ddbClient := Some(ddbClient),
159
+ kmsClient := Some (kmsClient)
160
+ );
161
+
162
+ var store :- expect KeyStore. KeyStore (keyStoreConfig);
163
+ return store;
164
+ }
165
+
166
+
144
167
method GetEmptyBeacons () returns (output : BeaconVersion)
145
168
ensures output. keyStore. ValidState ()
146
169
ensures fresh (output. keyStore. Modifies)
@@ -177,6 +200,24 @@ module BeaconTestFixtures {
177
200
);
178
201
}
179
202
203
+ method GetLotsaBeaconsMulti () returns (output : BeaconVersion)
204
+ ensures output. keyStore. ValidState ()
205
+ ensures fresh (output. keyStore. Modifies)
206
+ ensures output. version == 1
207
+ {
208
+ var store := GetMultiKeyStore ();
209
+ return BeaconVersion (
210
+ version := 1,
211
+ keyStore := store,
212
+ keySource := multi(MultiKeyStore(keyFieldName := "TheKeyField", cacheTTL := 42)),
213
+ standardBeacons := [std2, std4, std6, NameTitleBeacon, NameB, TitleB],
214
+ compoundBeacons := Some ([NameTitle, YearName, Mixed, JustSigned]),
215
+ virtualFields := Some ([NameTitleField]),
216
+ encryptedParts := None,
217
+ signedParts := None
218
+ );
219
+ }
220
+
180
221
const EmptyTableConfig := DynamoDbTableEncryptionConfig (
181
222
logicalTableName := "Foo",
182
223
partitionKeyName := "foo",
@@ -200,7 +241,8 @@ module BeaconTestFixtures {
200
241
"Title" := SE. ENCRYPT_AND_SIGN,
201
242
"TooBad" := SE. ENCRYPT_AND_SIGN,
202
243
"Year" := SE. SIGN_ONLY,
203
- "Date" := SE. SIGN_ONLY
244
+ "Date" := SE. SIGN_ONLY,
245
+ "TheKeyField" := SE. SIGN_ONLY
204
246
]
205
247
)
206
248
@@ -223,6 +265,26 @@ module BeaconTestFixtures {
223
265
return SI. KeySource (client, version.keyStore, SI.LiteralLoc(keys), cache, 0);
224
266
}
225
267
268
+ datatype KeyLocation =
269
+ | LiteralLoc (keys: HmacKeyMap )
270
+ | SingleLoc (keyId: string )
271
+ | MultiLoc (keyName : string , deleteKey : bool )
272
+
273
+ method GetMultiSource (keyName : string , version : BeaconVersion ) returns (output : SI. KeySource)
274
+ requires version. keyStore. ValidState ()
275
+ ensures output. ValidState ()
276
+ ensures version. keyStore == output. store
277
+ ensures fresh (output. client. Modifies)
278
+ {
279
+ var client :- expect Primitives. AtomicPrimitives ();
280
+ var mpl :- expect MaterialProviders. MaterialProviders ();
281
+ var input := MPT. CreateCryptographicMaterialsCacheInput (
282
+ cache := MPT.Default(Default := MPT.DefaultCache(entryCapacity := 3))
283
+ );
284
+ var cache :- expect mpl. CreateCryptographicMaterialsCache (input);
285
+ return SI. KeySource (client, version.keyStore, SI.MultiLoc(keyName, false), cache, 0);
286
+ }
287
+
226
288
const SimpleItem : DDB. AttributeMap := map [
227
289
"std2" := Std2String,
228
290
"std4" := Std4String,
0 commit comments