Skip to content
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.

Commit 9f84eb9

Browse files
RitvikKapilaRitvikKapila
committedDec 13, 2024·
updates
1 parent 071263d commit 9f84eb9

25 files changed

+166
-157
lines changed
 

‎DynamoDbEncryption/dafny/DynamoDbEncryption/Model/AwsCryptographyDbEncryptionSdkDynamoDbTypes.dfy

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -17,7 +17,7 @@ module {:extern "software.amazon.cryptography.dbencryptionsdk.dynamodb.internald
1717
import AwsCryptographyKeyStoreTypes
1818
import AwsCryptographyPrimitivesTypes
1919
import ComAmazonawsDynamodbTypes
20-
// Generic helpers for verification of mock/unit tests.
20+
// Generic helpers for verification of mock/unit tests.
2121
datatype DafnyCallEvent<I, O> = DafnyCallEvent(input: I, output: O)
2222

2323
// Begin Generated Types

‎DynamoDbEncryption/dafny/DynamoDbEncryption/Model/DynamoDbEncryption.smithy

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -719,7 +719,7 @@ structure SingleKeyStore {
719719
cacheTTL: Integer,
720720
@documentation("Provide the Shared Cache for Searchable Encryption.")
721721
cache : CacheType,
722-
@documentation("Partition ID to distinguish Beacon Key Sources writing to a cache. If the Partition ID is the same for two Beacon Key Sources, they can share the same cache entries in the cache.")
722+
@documentation("Partition ID to distinguish Beacon Key Sources writing to a Shared cache. If the Partition ID is the same for two Beacon Key Sources, they can share the same cache entries in the Shared cache.")
723723
partitionId: String
724724
}
725725

@@ -740,7 +740,7 @@ structure MultiKeyStore {
740740
cacheTTL: Integer,
741741
@javadoc("Which type of local cache to use.")
742742
cache : CacheType,
743-
@documentation("Partition ID to distinguish Beacon Key Sources writing to a cache. If the Partition ID is the same for two Beacon Key Sources, they can share the same cache entries in the cache.")
743+
@documentation("Partition ID to distinguish Beacon Key Sources writing to a Shared cache. If the Partition ID is the same for two Beacon Key Sources, they can share the same cache entries in the Shared cache.")
744744
partitionId: String
745745
}
746746

‎DynamoDbEncryption/dafny/DynamoDbEncryption/src/Beacon.dfy

Lines changed: 14 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -236,14 +236,14 @@ module BaseBeacon {
236236
//# [AttributeValue](https://docs.aws.amazon.com/amazondynamodb/latest/APIReference/API_AttributeValue.html)
237237
//# MUST be type "SS" StringSet.
238238
&& (ret.value.Some? ==> ret.value.value.SS?)
239-
//= specification/searchable-encryption/beacons.md#value-for-a-set-standard-beacon
240-
//= type=implication
241-
//# * The resulting set MUST NOT contain duplicates.
239+
//= specification/searchable-encryption/beacons.md#value-for-a-set-standard-beacon
240+
//= type=implication
241+
//# * The resulting set MUST NOT contain duplicates.
242242
&& (ret.value.Some? ==> HasNoDuplicates(ret.value.value.SS))
243-
//= specification/searchable-encryption/beacons.md#asset-initialization
244-
//= type=implication
245-
//# * Writing an item MUST fail if the item contains this beacon's attribute,
246-
//# and that attribute is not of type Set.
243+
//= specification/searchable-encryption/beacons.md#asset-initialization
244+
//= type=implication
245+
//# * Writing an item MUST fail if the item contains this beacon's attribute,
246+
//# and that attribute is not of type Set.
247247
&& var value := TermLoc.TermToAttr(loc, item, None);
248248
&& (value.Some? && !(value.value.SS? || value.value.NS? || value.value.BS?) ==> ret.Failure?)
249249
{
@@ -272,14 +272,14 @@ module BaseBeacon {
272272
//= type=implication
273273
//# * This operation MUST return no value if the associated field does not exist in the record
274274
&& (bytes.None? ==> ret.value.None?)
275-
//= specification/searchable-encryption/beacons.md#value-for-a-non-set-standard-beacon
276-
//= type=implication
277-
//# * This operation MUST convert the attribute value of the associated field to
278-
//# a sequence of bytes, as per [attribute serialization](../dynamodb-encryption-client/ddb-attribute-serialization.md).
275+
//= specification/searchable-encryption/beacons.md#value-for-a-non-set-standard-beacon
276+
//= type=implication
277+
//# * This operation MUST convert the attribute value of the associated field to
278+
//# a sequence of bytes, as per [attribute serialization](../dynamodb-encryption-client/ddb-attribute-serialization.md).
279279
&& (bytes.Some? ==> ret.value.Some? && hash(bytes.value, key).Success? && ret.value.value == DDB.AttributeValue.S(hash(bytes.value, key).value))
280-
//= specification/searchable-encryption/beacons.md#value-for-a-non-set-standard-beacon
281-
//= type=implication
282-
//# * This operation MUST return the [basicHash](#basichash) of the resulting bytes and the configured [beacon length](#beacon-length).
280+
//= specification/searchable-encryption/beacons.md#value-for-a-non-set-standard-beacon
281+
//= type=implication
282+
//# * This operation MUST return the [basicHash](#basichash) of the resulting bytes and the configured [beacon length](#beacon-length).
283283
&& (bytes.Some? ==> ret.value.Some? && base.hash(bytes.value, key, length).Success? && ret.value.value == DDB.AttributeValue.S(base.hash(bytes.value, key, length).value))
284284
{
285285
var bytes :- VirtToBytes(loc, item, vf);

‎DynamoDbEncryption/dafny/DynamoDbEncryption/src/CompoundBeacon.dfy

Lines changed: 9 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -397,9 +397,9 @@ module CompoundBeacon {
397397
//= type=implication
398398
//# * If a string is returned, it MUST NOT be empty.
399399
&& |res.value.value| > 0
400-
//= specification/searchable-encryption/beacons.md#value-for-a-compound-beacon
401-
//= type=implication
402-
//# * This operation MUST iterate through all constructors, in order, using the first that succeeds.
400+
//= specification/searchable-encryption/beacons.md#value-for-a-compound-beacon
401+
//= type=implication
402+
//# * This operation MUST iterate through all constructors, in order, using the first that succeeds.
403403
&& TryConstructors(construct, item, vf, keys).Success?
404404
{
405405
TryConstructors(construct, item, vf, keys)
@@ -578,9 +578,9 @@ module CompoundBeacon {
578578
ensures part.Signed? && ret.Success? ==>
579579
&& ret.value == part.prefix + data
580580
&& 0 < |ret.value|
581-
//= specification/searchable-encryption/beacons.md#value-for-a-compound-beacon
582-
//= type=implication
583-
//# * This operation MUST fail if any plaintext value used in the construction contains the split character.
581+
//= specification/searchable-encryption/beacons.md#value-for-a-compound-beacon
582+
//= type=implication
583+
//# * This operation MUST fail if any plaintext value used in the construction contains the split character.
584584
&& split !in data
585585

586586
//= specification/searchable-encryption/beacons.md#part-value-calculation
@@ -593,9 +593,9 @@ module CompoundBeacon {
593593
&& keys.Keys?
594594
&& part.beacon.hashStr(data, keys.value).Success?
595595
&& ret.value == part.prefix + part.beacon.hashStr(data, keys.value).value
596-
//= specification/searchable-encryption/beacons.md#value-for-a-compound-beacon
597-
//= type=implication
598-
//# * This operation MUST fail if any plaintext value used in the construction contains the split character.
596+
//= specification/searchable-encryption/beacons.md#value-for-a-compound-beacon
597+
//= type=implication
598+
//# * This operation MUST fail if any plaintext value used in the construction contains the split character.
599599
&& split !in data
600600
{
601601
:- Need(split !in data, E("Value '" + data + "' for beacon part " + part.getName() + " contains the split character '" + [split] + "'."));

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

Lines changed: 20 additions & 27 deletions
Original file line numberDiff line numberDiff line change
@@ -33,7 +33,6 @@ module SearchConfigToInfo {
3333
import SE = AwsCryptographyDbEncryptionSdkStructuredEncryptionTypes
3434
import MPT = AwsCryptographyMaterialProvidersTypes
3535
import Primitives = AtomicPrimitives
36-
import UUID
3736

3837
// convert configured SearchConfig to internal SearchInfo
3938
method Convert(outer : DynamoDbTableEncryptionConfig)
@@ -165,7 +164,7 @@ module SearchConfigToInfo {
165164
)
166165
);
167166
}
168-
if config.single? && config.single.partitionId.Some? {
167+
else if config.single? && config.single.partitionId.Some? {
169168
partitionIdBytes :- UTF8.Encode(config.single.partitionId.value)
170169
.MapFailure(
171170
e => Error.DynamoDbEncryptionException(
@@ -174,13 +173,7 @@ module SearchConfigToInfo {
174173
);
175174
}
176175
else {
177-
var uuid? := UUID.GenerateUUID();
178-
179-
var uuid :- uuid?
180-
.MapFailure(e => Error.DynamoDbEncryptionException(message := e));
181-
182-
partitionIdBytes :- UUID.ToByteArray(uuid)
183-
.MapFailure(e => Error.DynamoDbEncryptionException(message := e));
176+
partitionIdBytes :- I.GeneratePartitionId();
184177
}
185178

186179
if config.multi? {
@@ -511,10 +504,10 @@ module SearchConfigToInfo {
511504
//= type=implication
512505
//# Initialization MUST fail if two standard beacons are configured with the same location.
513506
&& FindBeaconWithThisLocation(converted, loc).None?
514-
//= specification/searchable-encryption/virtual.md#virtual-field-initialization
515-
//= type=implication
516-
//# Initialization MUST fail if a virtual field is defined with only one location,
517-
//# and also a [standard beacon](beacons.md#standard-beacon) is defined with that same location.
507+
//= specification/searchable-encryption/virtual.md#virtual-field-initialization
508+
//= type=implication
509+
//# Initialization MUST fail if a virtual field is defined with only one location,
510+
//# and also a [standard beacon](beacons.md#standard-beacon) is defined with that same location.
518511
&& FindVirtualFieldWithThisLocation(virtualFields, {loc}).None?
519512
{
520513
if |beacons| == 0 {
@@ -643,10 +636,10 @@ module SearchConfigToInfo {
643636
//# or is not `signed`.
644637
ensures
645638
(&& 0 < |parts|
646-
//= specification/searchable-encryption/beacons.md#signed-part-initialization
647-
//= type=implication
648-
//# If no [terminal location](virtual.md#terminal-location) is provided,
649-
//# the `name` MUST be used as the [terminal location](virtual.md#terminal-location).
639+
//= specification/searchable-encryption/beacons.md#signed-part-initialization
640+
//= type=implication
641+
//# If no [terminal location](virtual.md#terminal-location) is provided,
642+
//# the `name` MUST be used as the [terminal location](virtual.md#terminal-location).
650643
&& GetLoc(parts[0].name, parts[0].loc).Success?
651644
&& var loc := GetLoc(parts[0].name, parts[0].loc).value;
652645
&& !IsSignOnly(outer, CB.Signed(parts[0].prefix, parts[0].name, loc).loc))
@@ -728,10 +721,10 @@ module SearchConfigToInfo {
728721
ensures ret.Success? ==>
729722
&& |ret.value| == 1
730723
&& |ret.value[0].parts| == |parts| + |converted|
731-
//= specification/searchable-encryption/beacons.md#default-construction
732-
//= type=implication
733-
//# * This default constructor MUST be all of the signed parts,
734-
//# followed by all the encrypted parts, all parts being required.
724+
//= specification/searchable-encryption/beacons.md#default-construction
725+
//= type=implication
726+
//# * This default constructor MUST be all of the signed parts,
727+
//# followed by all the encrypted parts, all parts being required.
735728
&& CB.OrderedParts(allParts, numNon)
736729
&& (forall i | 0 <= i < |ret.value[0].parts| ::
737730
&& ret.value[0].parts[i].part == allParts[i]
@@ -1116,14 +1109,14 @@ module SearchConfigToInfo {
11161109
ensures ret.Success? && 0 < |names| && data[names[0]].Standard? && data[names[0]].std.share.Some? ==>
11171110
&& var share := data[names[0]].std.share.value;
11181111
&& IsValidShare(data, names[0], data[names[0]].std.length, share).Success?
1119-
//= specification/searchable-encryption/beacons.md#shared-initialization
1120-
//= type=implication
1121-
//# This name MUST be the name of a previously defined Standard Beacon.
1112+
//= specification/searchable-encryption/beacons.md#shared-initialization
1113+
//= type=implication
1114+
//# This name MUST be the name of a previously defined Standard Beacon.
11221115
&& share in data
11231116
&& data[share].Standard?
1124-
//= specification/searchable-encryption/beacons.md#shared-initialization
1125-
//= type=implication
1126-
//# This beacon's [length](#beacon-length) MUST be equal to the `other` beacon's [length](#beacon-length).
1117+
//= specification/searchable-encryption/beacons.md#shared-initialization
1118+
//= type=implication
1119+
//# This beacon's [length](#beacon-length) MUST be equal to the `other` beacon's [length](#beacon-length).
11271120
&& data[share].std.length == data[names[0]].std.length
11281121
{
11291122
if |names| == 0 then

‎DynamoDbEncryption/dafny/DynamoDbEncryption/src/DynamoToStruct.dfy

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -584,10 +584,10 @@ module DynamoToStruct {
584584
ensures ret.Success? ==>
585585
&& U32ToBigEndian(|b|).Success?
586586
&& |ret.value| == LENGTH_LEN + |b|
587-
//= specification/dynamodb-encryption-client/ddb-attribute-serialization.md#set-entry-length
588-
//= type=implication
589-
//# Set Entry Length MUST be a big-endian unsigned integer
590-
//# equal to the length of [Set Entry Value](#set-entry-value).
587+
//= specification/dynamodb-encryption-client/ddb-attribute-serialization.md#set-entry-length
588+
//= type=implication
589+
//# Set Entry Length MUST be a big-endian unsigned integer
590+
//# equal to the length of [Set Entry Value](#set-entry-value).
591591
&& ret.value[0..LENGTH_LEN] == U32ToBigEndian(|b|).value
592592
&& ret.value[LENGTH_LEN..] == b
593593
{

‎DynamoDbEncryption/dafny/DynamoDbEncryption/src/FilterExpr.dfy

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1289,9 +1289,9 @@ module DynamoDBFilterExpr {
12891289
a[0] < b[0]
12901290
else
12911291
bIsHighSurrogate
1292-
// we know aIsHighSurrogate != bIsHighSurrogate and a[0] != b[0]
1293-
// so if bIsHighSurrogate then a is less
1294-
// and if aIsHighSurrogate then a is greater
1292+
// we know aIsHighSurrogate != bIsHighSurrogate and a[0] != b[0]
1293+
// so if bIsHighSurrogate then a is less
1294+
// and if aIsHighSurrogate then a is greater
12951295
}
12961296

12971297
predicate method UnicodeLessOrEqual(a : string, b : string)

‎DynamoDbEncryption/dafny/DynamoDbEncryption/src/SearchInfo.dfy

Lines changed: 33 additions & 17 deletions
Original file line numberDiff line numberDiff line change
@@ -27,6 +27,7 @@ module SearchableEncryptionInfo {
2727
import KeyStoreTypes = AwsCryptographyKeyStoreTypes
2828
import SE = AwsCryptographyDbEncryptionSdkStructuredEncryptionTypes
2929
import opened CacheConstants
30+
import UUID
3031

3132
//= specification/searchable-encryption/search-config.md#version-number
3233
//= type=implication
@@ -72,11 +73,11 @@ module SearchableEncryptionInfo {
7273
//# MUST be generated in accordance with [HMAC Key Generation](#hmac-key-generation).
7374
var newKey :- GetBeaconKey(client, key, keysLeft[0]);
7475
reveal Seq.HasNoDuplicates();
75-
//= specification/searchable-encryption/search-config.md#get-beacon-key-materials
76-
//# [Beacon Key Materials](../../submodules/MaterialProviders/aws-encryption-sdk-specification/framework/structures.md#beacon-key-materials) MUST be generated
77-
//# with the [beacon key id](#beacon-key-id) equal to the `beacon key id`
78-
//# and the [HMAC Keys](../../submodules/MaterialProviders/aws-encryption-sdk-specification/framework/structures.md#hmac-keys) equal to a map
79-
//# of every [standard beacons](beacons.md#standard-beacon-initialization) name to its generated HMAC key.
76+
//= specification/searchable-encryption/search-config.md#get-beacon-key-materials
77+
//# [Beacon Key Materials](../../submodules/MaterialProviders/aws-encryption-sdk-specification/framework/structures.md#beacon-key-materials) MUST be generated
78+
//# with the [beacon key id](#beacon-key-id) equal to the `beacon key id`
79+
//# and the [HMAC Keys](../../submodules/MaterialProviders/aws-encryption-sdk-specification/framework/structures.md#hmac-keys) equal to a map
80+
//# of every [standard beacons](beacons.md#standard-beacon-initialization) name to its generated HMAC key.
8081
output := GetHmacKeys(client, allKeys, keysLeft[1..], key, acc[keysLeft[0] := newKey]);
8182
}
8283
}
@@ -106,14 +107,14 @@ module SearchableEncryptionInfo {
106107
&& hkdfInput.digestAlgorithm == Prim.SHA_512
107108
&& hkdfInput.salt == None
108109
&& hkdfInput.ikm == key
109-
//= specification/searchable-encryption/search-config.md#hmac-key-generation
110-
//= type=implication
111-
//# The `info` MUST be the concatenation of "AWS_DBE_SCAN_BEACON" encoded as UTF8
112-
//# and the beacon name.
110+
//= specification/searchable-encryption/search-config.md#hmac-key-generation
111+
//= type=implication
112+
//# The `info` MUST be the concatenation of "AWS_DBE_SCAN_BEACON" encoded as UTF8
113+
//# and the beacon name.
113114
&& hkdfInput.info == info
114-
//= specification/searchable-encryption/search-config.md#hmac-key-generation
115-
//= type=implication
116-
//# The `expectedLength` MUST be 64 bytes.
115+
//= specification/searchable-encryption/search-config.md#hmac-key-generation
116+
//= type=implication
117+
//# The `expectedLength` MUST be 64 bytes.
117118
&& hkdfInput.expectedLength == 64
118119
{
119120
var info :- UTF8.Encode("AWS_DBE_SCAN_BEACON" + name).MapFailure(e => E(e));
@@ -128,6 +129,20 @@ module SearchableEncryptionInfo {
128129
return Success(newKey);
129130
}
130131

132+
// Generates a new partitionId, which is a random UUID
133+
method GeneratePartitionId() returns (output : Result<seq<uint8>, Error>)
134+
{
135+
var uuid? := UUID.GenerateUUID();
136+
137+
var uuid :- uuid?
138+
.MapFailure(e => Error.DynamoDbEncryptionException(message := e));
139+
140+
var partitionIdBytes: seq<uint8> :- UUID.ToByteArray(uuid)
141+
.MapFailure(e => Error.DynamoDbEncryptionException(message := e));
142+
143+
output := Success(partitionIdBytes);
144+
}
145+
131146
datatype KeyLocation =
132147
| LiteralLoc (keys: HmacKeyMap)
133148
| SingleLoc (keyId: string)
@@ -219,6 +234,7 @@ module SearchableEncryptionInfo {
219234
&& var cacheInput := Seq.Last(newHistory).input;
220235
&& var cacheOutput := Seq.Last(newHistory).output;
221236
&& UTF8.Encode(keyId).Success?
237+
// TODO - why is this verifying?
222238
&& cacheInput.identifier == UTF8.Encode(keyId).value
223239

224240
//= specification/searchable-encryption/search-config.md#get-beacon-key-materials
@@ -234,9 +250,9 @@ module SearchableEncryptionInfo {
234250
&& var oldGetHistory := old(store.History.GetBeaconKey);
235251
&& var newGetHistory := store.History.GetBeaconKey;
236252
&& |newGetHistory| == |oldGetHistory|+1
237-
//= specification/searchable-encryption/search-config.md#get-beacon-key-materials
238-
//= type=implication
239-
//# If `GetBeaconKey` fails get beacon key MUST fail.
253+
//= specification/searchable-encryption/search-config.md#get-beacon-key-materials
254+
//= type=implication
255+
//# If `GetBeaconKey` fails get beacon key MUST fail.
240256
&& Seq.Last(newGetHistory).output.Success?
241257
&& var storeInput := Seq.Last(newGetHistory).input;
242258
&& var storeOutput := Seq.Last(newGetHistory).output;
@@ -258,7 +274,7 @@ module SearchableEncryptionInfo {
258274
)
259275
{
260276

261-
// Resource ID: Searchable Encryption [0x02]
277+
// Resource ID: Hierarchical Keyring [0x02]
262278
var resourceId : seq<uint8> := RESOURCE_ID_HIERARCHICAL_KEYRING;
263279

264280
// Scope ID: Searchable Encryption [0x03]
@@ -318,7 +334,7 @@ module SearchableEncryptionInfo {
318334
//# equal to now + configured [cacheTTL](#cachettl).
319335
var now := Time.GetCurrent();
320336
var putCacheEntryInput:= MP.PutCacheEntryInput(
321-
identifier := keyIdBytes,
337+
identifier := identifier,
322338
materials := MP.Materials.BeaconKey(beaconKeyMaterials),
323339
creationTime := now,
324340
expiryTime := now+cacheTTL as MP.PositiveLong,

‎DynamoDbEncryption/dafny/DynamoDbEncryption/src/Virtual.dfy

Lines changed: 11 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -171,10 +171,10 @@ module DdbVirtualFields {
171171
//# If the position provided is positive, it MUST be the zero-based index from the start of the list.
172172
&& (0 <= pos < limit ==> ret == pos)
173173
&& (limit <= pos ==> ret == limit-1)
174-
//= specification/searchable-encryption/virtual.md#position-definition
175-
//= type=implication
176-
//# If the position provided is negative, it's absolute value MUST be the
177-
//# one-based index from the end of the list, that is, -1 refers to the last item in the list.
174+
//= specification/searchable-encryption/virtual.md#position-definition
175+
//= type=implication
176+
//# If the position provided is negative, it's absolute value MUST be the
177+
//# one-based index from the end of the list, that is, -1 refers to the last item in the list.
178178
&& (0 < -pos < limit ==> ret == limit + pos)
179179
&& (limit <= -pos ==> ret == 0)
180180
{
@@ -259,10 +259,10 @@ module DdbVirtualFields {
259259
//= type=implication
260260
//# If index is greater than the number of items in the list, an empty string MUST be returned.
261261
&& (index >= |parts| || -index > |parts| ==> ret == "")
262-
//= specification/searchable-encryption/virtual.md#getsegment-transform-initialization
263-
//= type=implication
264-
//# The GetSegment transform MUST split the input string on the given character,
265-
//# and return the item in the resulting list the corresponds to the given position.
262+
//= specification/searchable-encryption/virtual.md#getsegment-transform-initialization
263+
//= type=implication
264+
//# The GetSegment transform MUST split the input string on the given character,
265+
//# and return the item in the resulting list the corresponds to the given position.
266266
&& (index < |parts| && -index <= |parts| ==> ret == parts[GetPos(index, |parts|)])
267267
{
268268
var parts := Split(s, split);
@@ -285,9 +285,9 @@ module DdbVirtualFields {
285285
//# GetSegments MUST return the range of parts from low (inclusive) to high (exclusive),
286286
//# joined on the `split` character.
287287
&& (lo < hi ==> ret == Join(parts[lo..hi], [split]))
288-
//= specification/searchable-encryption/virtual.md#getsegments-transform-initialization
289-
//= type=implication
290-
//# If high is less than or equal to low, an empty string MUST be returned.
288+
//= specification/searchable-encryption/virtual.md#getsegments-transform-initialization
289+
//= type=implication
290+
//# If high is less than or equal to low, an empty string MUST be returned.
291291
&& (lo >= hi ==> ret == "")
292292
{
293293
var parts := Split(s, split);

‎DynamoDbEncryption/dafny/DynamoDbEncryption/test/BeaconTestFixtures.dfy

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -243,11 +243,11 @@ module BeaconTestFixtures {
243243
);
244244
var cache :- expect mpl.CreateCryptographicMaterialsCache(input);
245245
// Create a test partitionIdBytes
246-
var partitionIdBytes : seq<uint8> := [1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16];
246+
var partitionIdBytes : seq<uint8> :- expect SI.GeneratePartitionId();
247247
return SI.KeySource(client, version.keyStore, SI.LiteralLoc(keys), cache, 0, partitionIdBytes);
248248
}
249249

250-
method GetMultiSource(keyName : string, version : BeaconVersion) returns (output : SI.KeySource)
250+
method GetMultiSource(keyName : string, version : BeaconVersion, partitionId: Option<seq<uint8>>, shared_cache: Option<MPT.ICryptographicMaterialsCache>) returns (output : SI.KeySource)
251251
requires version.keyStore.ValidState()
252252
ensures output.ValidState()
253253
ensures version.keyStore == output.store
@@ -260,7 +260,7 @@ module BeaconTestFixtures {
260260
);
261261
var cache :- expect mpl.CreateCryptographicMaterialsCache(input);
262262
// Create a test partitionIdBytes
263-
var partitionIdBytes : seq<uint8> := [1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16];
263+
var partitionIdBytes : seq<uint8> :- expect SI.GeneratePartitionId();
264264
return SI.KeySource(client, version.keyStore, SI.MultiLoc(keyName, false), cache, 0, partitionIdBytes);
265265
}
266266

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -17,7 +17,7 @@ module {:extern "software.amazon.cryptography.dbencryptionsdk.dynamodb.transform
1717
import AwsCryptographyDbEncryptionSdkStructuredEncryptionTypes
1818
import AwsCryptographyMaterialProvidersTypes
1919
import ComAmazonawsDynamodbTypes
20-
// Generic helpers for verification of mock/unit tests.
20+
// Generic helpers for verification of mock/unit tests.
2121
datatype DafnyCallEvent<I, O> = DafnyCallEvent(input: I, output: O)
2222

2323
// Begin Generated Types

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

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -72,9 +72,9 @@ module DdbMiddlewareConfig {
7272
{
7373
&& (forall tableName <- config.tableEncryptionConfigs ::
7474
config.tableEncryptionConfigs[tableName].physicalTableName == tableName)
75-
//= specification/dynamodb-encryption-client/ddb-table-encryption-config.md#logical-table-name
76-
//# When mapping [DynamoDB Table Names](#dynamodb-table-name) to [logical table name](#logical-table-name)
77-
//# there MUST a one to one mapping between the two.
75+
//= specification/dynamodb-encryption-client/ddb-table-encryption-config.md#logical-table-name
76+
//# When mapping [DynamoDB Table Names](#dynamodb-table-name) to [logical table name](#logical-table-name)
77+
//# there MUST a one to one mapping between the two.
7878
&& (forall
7979
c1 <- config.tableEncryptionConfigs.Values,
8080
c2 <- config.tableEncryptionConfigs.Values

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

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -128,11 +128,11 @@ module DynamoDbMiddlewareSupport {
128128
(ret : Result<Option<string>, Error>)
129129
ensures ret.Success? && config.search.Some? && config.search.value.curr().keySource.keyLoc.MultiLoc? ==>
130130
&& output.parsedHeader.Some?
131-
//= specification/searchable-encryption/search-config.md#get-beacon-key-id-from-parsed-header
132-
//= type=implication
133-
//# If the [Parsed Header](../dynamodb-encryption-client/encrypt-item.md#parsed-header)'s encrypted data keys
134-
//# do not contain only one encrypted data key
135-
//# this function MUST fail.
131+
//= specification/searchable-encryption/search-config.md#get-beacon-key-id-from-parsed-header
132+
//= type=implication
133+
//# If the [Parsed Header](../dynamodb-encryption-client/encrypt-item.md#parsed-header)'s encrypted data keys
134+
//# do not contain only one encrypted data key
135+
//# this function MUST fail.
136136
&& var keys := output.parsedHeader.value.encryptedDataKeys;
137137
&& |keys| == 1
138138

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

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -188,8 +188,8 @@ module UpdateItemTransform {
188188
|| input.originalInput.ReturnValues.value.ALL_OLD?)
189189
)
190190
{
191-
// This error should not be possible to reach if we assume the DDB API contract is correct.
192-
// We include this runtime check for defensive purposes.
191+
// This error should not be possible to reach if we assume the DDB API contract is correct.
192+
// We include this runtime check for defensive purposes.
193193
:- Need(forall k <- attributes.Keys :: !IsSigned(tableConfig, k),
194194
E("UpdateItems response contains signed attributes, but does not include the entire item which is required for verification."));
195195

‎DynamoDbEncryption/dafny/DynamoDbItemEncryptor/Model/AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorTypes.dfy

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -17,7 +17,7 @@ module {:extern "software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencry
1717
import AwsCryptographyMaterialProvidersTypes
1818
import AwsCryptographyPrimitivesTypes
1919
import ComAmazonawsDynamodbTypes
20-
// Generic helpers for verification of mock/unit tests.
20+
// Generic helpers for verification of mock/unit tests.
2121
datatype DafnyCallEvent<I, O> = DafnyCallEvent(input: I, output: O)
2222

2323
// Begin Generated Types

‎DynamoDbEncryption/dafny/DynamoDbItemEncryptor/src/AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations.dfy

Lines changed: 12 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -54,11 +54,11 @@ module AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations refines Abs
5454
|| (unauthenticatedAttributes.Some? && attr in unauthenticatedAttributes.value)
5555
|| (unauthenticatedPrefix.Some? && unauthenticatedPrefix.value <= attr)
5656
|| ReservedPrefix <= attr
57-
// Attributes with the reserved prefix are "allowed unauthenticated" in that
58-
// they are not specified as signed within attributeActionsOnEncrypt.
59-
// These attributes MAY still be authenticated via other methods,
60-
// such as "aws_dbe_head" which is explicitly added to the canonical hash
61-
// used in signing.
57+
// Attributes with the reserved prefix are "allowed unauthenticated" in that
58+
// they are not specified as signed within attributeActionsOnEncrypt.
59+
// These attributes MAY still be authenticated via other methods,
60+
// such as "aws_dbe_head" which is explicitly added to the canonical hash
61+
// used in signing.
6262
}
6363

6464
//= specification/dynamodb-encryption-client/decrypt-item.md#signature-scope
@@ -126,9 +126,9 @@ module AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations refines Abs
126126
{
127127
&& InSignatureScope(config, attr)
128128
&& attr !in config.attributeActionsOnEncrypt
129-
// Attributes in signature scope MUST be configured in attributeActionsOnEncrypt
130-
// so these two lines are saying "in scope && not in scope"
131-
// and that's why it's an error
129+
// Attributes in signature scope MUST be configured in attributeActionsOnEncrypt
130+
// so these two lines are saying "in scope && not in scope"
131+
// and that's why it's an error
132132
}
133133

134134
// Is the attribute name in signature scope?
@@ -176,9 +176,9 @@ module AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations refines Abs
176176
//= type=implication
177177
//# If the Version Number is 2, then the base context MUST be the [version 2](./encrypt-item.md#dynamodb-item-base-context-version-2) context.
178178
&& (header[0] == 2 ==> ret == MakeEncryptionContextV2(config, item))
179-
//= specification/dynamodb-encryption-client/decrypt-item.md#dynamodb-item-base-context
180-
//= type=implication
181-
//# If the Version Number is 1, the base context MUST be the [version 1](./encrypt-item.md#dynamodb-item-base-context-version-1) context.
179+
//= specification/dynamodb-encryption-client/decrypt-item.md#dynamodb-item-base-context
180+
//= type=implication
181+
//# If the Version Number is 1, the base context MUST be the [version 1](./encrypt-item.md#dynamodb-item-base-context-version-1) context.
182182
&& (header[0] == 1 ==> ret == MakeEncryptionContextV1(config, item))
183183
&& ((header[0] == 1) || (header[0] == 2))
184184

@@ -441,7 +441,7 @@ module AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations refines Abs
441441
// The partition key MUST be CSE.SIGN_ONLY
442442
&& config.partitionKeyName in config.attributeActionsOnEncrypt
443443
&& config.attributeActionsOnEncrypt[config.partitionKeyName] == KeyActionFromVersion(config.version)
444-
// The sort key MUST be CSE.SIGN_ONLY
444+
// The sort key MUST be CSE.SIGN_ONLY
445445
&& (config.sortKeyName.Some? ==>
446446
&& config.sortKeyName.value in config.attributeActionsOnEncrypt
447447
&& config.attributeActionsOnEncrypt[config.sortKeyName.value] == KeyActionFromVersion(config.version))

‎DynamoDbEncryption/dafny/StructuredEncryption/Model/AwsCryptographyDbEncryptionSdkStructuredEncryptionTypes.dfy

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -11,7 +11,7 @@ module {:extern "software.amazon.cryptography.dbencryptionsdk.structuredencrypti
1111
import opened UTF8
1212
import AwsCryptographyMaterialProvidersTypes
1313
import AwsCryptographyPrimitivesTypes
14-
// Generic helpers for verification of mock/unit tests.
14+
// Generic helpers for verification of mock/unit tests.
1515
datatype DafnyCallEvent<I, O> = DafnyCallEvent(input: I, output: O)
1616

1717
// Begin Generated Types

‎DynamoDbEncryption/dafny/StructuredEncryption/src/AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations.dfy

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -715,9 +715,9 @@ module AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations refines Abst
715715
assume {:axiom} input.cmm.Modifies !! {config.materialProviders.History};
716716
var newEncryptionContext :- GetV2EncryptionContext(input.plaintextStructure);
717717
if |newEncryptionContext| != 0 {
718-
//= specification/structured-encryption/encrypt-path-structure.md#create-new-encryption-context-and-cmm
719-
//# An error MUST be returned if any of the entries added to the encryption context in this step
720-
//# have the same key as any entry already in the encryption context.
718+
//= specification/structured-encryption/encrypt-path-structure.md#create-new-encryption-context-and-cmm
719+
//# An error MUST be returned if any of the entries added to the encryption context in this step
720+
//# have the same key as any entry already in the encryption context.
721721
:- Need(encryptionContext.Keys !! newEncryptionContext.Keys,
722722
E("Internal Error - Structured Encryption encryption context overlaps with Item Encryptor encryption context."));
723723
encryptionContext := encryptionContext + newEncryptionContext;
@@ -1070,9 +1070,9 @@ module AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations refines Abst
10701070
//# in the input record, plus the Legend.
10711071
var newEncryptionContext :- GetV2EncryptionContext(UnCanon(canonData));
10721072
if |newEncryptionContext| != 0 {
1073-
//= specification/structured-encryption/decrypt-path-structure.md#create-new-encryption-context-and-cmm
1074-
//# An error MUST be returned if any of the entries added to the encryption context in this step
1075-
//# have the same key as any entry already in the encryption context.
1073+
//= specification/structured-encryption/decrypt-path-structure.md#create-new-encryption-context-and-cmm
1074+
//# An error MUST be returned if any of the entries added to the encryption context in this step
1075+
//# have the same key as any entry already in the encryption context.
10761076
:- Need(encryptionContext.Keys !! newEncryptionContext.Keys,
10771077
E("Internal Error - Structured Encryption encryption context overlaps with Item Encryptor encryption context."));
10781078
encryptionContext := encryptionContext + newEncryptionContext;

‎DynamoDbEncryption/dafny/StructuredEncryption/src/Canonize.dfy

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -552,7 +552,7 @@ module {:options "/functionSyntax:4" } Canonize {
552552

553553
// This says vcs_split_on_every_assert, because it has many many asserts, each of which is cheap
554554
opaque function {:vcs_split_on_every_assert}
555-
DoResolveLegend(canonSorted : CanonAuthList, legend: Header.Legend, ghost tableName : GoodString, ghost data : AuthList) : (ret : Result<CanonCryptoList, Error>)
555+
DoResolveLegend(canonSorted : CanonAuthList, legend: Header.Legend, ghost tableName : GoodString, ghost data : AuthList) : (ret : Result<CanonCryptoList, Error>)
556556
requires CanonAuthMatchesAuthList(tableName, data, canonSorted)
557557
requires Relations.SortedBy(canonSorted, SortCanon.AuthBelow)
558558
ensures ret.Success? ==>

‎DynamoDbEncryption/dafny/StructuredEncryption/src/Crypt.dfy

Lines changed: 8 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -26,7 +26,7 @@ module StructuredEncryptionCrypt {
2626
import AesKdfCtr
2727
import Seq
2828
import SortCanon
29-
// import Relations
29+
// import Relations
3030
import opened Canonize
3131

3232
function method FieldKey(HKDFOutput : Bytes, offset : uint32)
@@ -455,9 +455,9 @@ module StructuredEncryptionCrypt {
455455
//# The `Cipherkey` MUST be the first 32 bytes of the `FieldKey`
456456
&& KeySize == 32
457457
&& encryptInput.key == fieldKey[0..KeySize]
458-
//= specification/structured-encryption/encrypt-path-structure.md#calculate-cipherkey-and-nonce
459-
//= type=implication
460-
//# The `Nonce` MUST be the remaining 12 bytes of the `FieldKey`
458+
//= specification/structured-encryption/encrypt-path-structure.md#calculate-cipherkey-and-nonce
459+
//= type=implication
460+
//# The `Nonce` MUST be the remaining 12 bytes of the `FieldKey`
461461
&& NonceSize == 12
462462
&& |fieldKey| - KeySize == 12
463463
&& encryptInput.iv == fieldKey[KeySize..]
@@ -510,10 +510,10 @@ module StructuredEncryptionCrypt {
510510
returns (ret : Result<StructuredDataTerminal, Error>)
511511
ensures ret.Success? ==>
512512
&& |data.value| >= (AuthTagSize+2)
513-
//= specification/structured-encryption/decrypt-path-structure.md#terminal-data-decryption
514-
//= type=implication
515-
//# The output Terminal Data MUST have a [Terminal Type Id](./structures.md#terminal-type-id)
516-
//# equal to the deserialized Terminal Type Id.
513+
//= specification/structured-encryption/decrypt-path-structure.md#terminal-data-decryption
514+
//= type=implication
515+
//# The output Terminal Data MUST have a [Terminal Type Id](./structures.md#terminal-type-id)
516+
//# equal to the deserialized Terminal Type Id.
517517
&& ret.value.typeId == data.value[0..TYPEID_LEN]
518518
&& ret.value != data
519519

‎DynamoDbEncryption/dafny/StructuredEncryption/src/Header.dfy

Lines changed: 15 additions & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -114,17 +114,17 @@ module StructuredEncryptionHeader {
114114
function method {:opaque} serialize() : (ret : Bytes)
115115
ensures
116116
&& PREFIX_LEN <= |ret|
117-
//= specification/structured-encryption/header.md#partial-header
118-
//= type=implication
119-
//# The Partial Header MUST be
120-
// | Length (bytes) | Meaning |
121-
// |---|---|
122-
// | 1 | [Format Version](#format-version) |
123-
// | 1 | [Format Flavor](#format-flavor) |
124-
// | 32 | [Message ID](#message-id) |
125-
// | Variable | [Encrypt Legend](#encrypt-legend) |
126-
// | Variable | [Encryption Context](#encryption-context) |
127-
// | Variable | [Encrypted Data Keys](#encrypted-data-keys) |
117+
//= specification/structured-encryption/header.md#partial-header
118+
//= type=implication
119+
//# The Partial Header MUST be
120+
// | Length (bytes) | Meaning |
121+
// |---|---|
122+
// | 1 | [Format Version](#format-version) |
123+
// | 1 | [Format Flavor](#format-flavor) |
124+
// | 32 | [Message ID](#message-id) |
125+
// | Variable | [Encrypt Legend](#encrypt-legend) |
126+
// | Variable | [Encryption Context](#encryption-context) |
127+
// | Variable | [Encrypted Data Keys](#encrypted-data-keys) |
128128
&& ret == (
129129
[version]
130130
+ [flavor]
@@ -321,10 +321,10 @@ module StructuredEncryptionHeader {
321321
requires ValidSuite(alg)
322322
ensures ret.Success? ==>
323323
&& |ret.value| == COMMITMENT_LEN
324-
//= specification/structured-encryption/header.md#commitment-calculation
325-
//= type=implication
326-
//# The Header Commitment MUST be calculated as a the first 32 bytes of an HmacSha384,
327-
//# with the serialized partial header as the message, and the Commit Key as the key.
324+
//= specification/structured-encryption/header.md#commitment-calculation
325+
//= type=implication
326+
//# The Header Commitment MUST be calculated as a the first 32 bytes of an HmacSha384,
327+
//# with the serialized partial header as the message, and the Commit Key as the key.
328328
&& var input := Prim.HMacInput(
329329
digestAlgorithm := alg.commitment.HKDF.hmac,
330330
key := commitKey,

‎DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/model/MultiKeyStore.java

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -27,7 +27,7 @@ public class MultiKeyStore {
2727
private final CacheType cache;
2828

2929
/**
30-
* Partition ID to distinguish Beacon Key Sources writing to a cache. If the Partition ID is the same for two Beacon Key Sources, they can share the same cache entries in the cache.
30+
* Partition ID to distinguish Beacon Key Sources writing to a Shared cache. If the Partition ID is the same for two Beacon Key Sources, they can share the same cache entries in the Shared cache.
3131
*/
3232
private final String partitionId;
3333

@@ -60,7 +60,7 @@ public CacheType cache() {
6060
}
6161

6262
/**
63-
* @return Partition ID to distinguish Beacon Key Sources writing to a cache. If the Partition ID is the same for two Beacon Key Sources, they can share the same cache entries in the cache.
63+
* @return Partition ID to distinguish Beacon Key Sources writing to a Shared cache. If the Partition ID is the same for two Beacon Key Sources, they can share the same cache entries in the Shared cache.
6464
*/
6565
public String partitionId() {
6666
return this.partitionId;
@@ -106,12 +106,12 @@ public interface Builder {
106106
CacheType cache();
107107

108108
/**
109-
* @param partitionId Partition ID to distinguish Beacon Key Sources writing to a cache. If the Partition ID is the same for two Beacon Key Sources, they can share the same cache entries in the cache.
109+
* @param partitionId Partition ID to distinguish Beacon Key Sources writing to a Shared cache. If the Partition ID is the same for two Beacon Key Sources, they can share the same cache entries in the Shared cache.
110110
*/
111111
Builder partitionId(String partitionId);
112112

113113
/**
114-
* @return Partition ID to distinguish Beacon Key Sources writing to a cache. If the Partition ID is the same for two Beacon Key Sources, they can share the same cache entries in the cache.
114+
* @return Partition ID to distinguish Beacon Key Sources writing to a Shared cache. If the Partition ID is the same for two Beacon Key Sources, they can share the same cache entries in the Shared cache.
115115
*/
116116
String partitionId();
117117

‎DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/model/SingleKeyStore.java

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -27,7 +27,7 @@ public class SingleKeyStore {
2727
private final CacheType cache;
2828

2929
/**
30-
* Partition ID to distinguish Beacon Key Sources writing to a cache. If the Partition ID is the same for two Beacon Key Sources, they can share the same cache entries in the cache.
30+
* Partition ID to distinguish Beacon Key Sources writing to a Shared cache. If the Partition ID is the same for two Beacon Key Sources, they can share the same cache entries in the Shared cache.
3131
*/
3232
private final String partitionId;
3333

@@ -60,7 +60,7 @@ public CacheType cache() {
6060
}
6161

6262
/**
63-
* @return Partition ID to distinguish Beacon Key Sources writing to a cache. If the Partition ID is the same for two Beacon Key Sources, they can share the same cache entries in the cache.
63+
* @return Partition ID to distinguish Beacon Key Sources writing to a Shared cache. If the Partition ID is the same for two Beacon Key Sources, they can share the same cache entries in the Shared cache.
6464
*/
6565
public String partitionId() {
6666
return this.partitionId;
@@ -106,12 +106,12 @@ public interface Builder {
106106
CacheType cache();
107107

108108
/**
109-
* @param partitionId Partition ID to distinguish Beacon Key Sources writing to a cache. If the Partition ID is the same for two Beacon Key Sources, they can share the same cache entries in the cache.
109+
* @param partitionId Partition ID to distinguish Beacon Key Sources writing to a Shared cache. If the Partition ID is the same for two Beacon Key Sources, they can share the same cache entries in the Shared cache.
110110
*/
111111
Builder partitionId(String partitionId);
112112

113113
/**
114-
* @return Partition ID to distinguish Beacon Key Sources writing to a cache. If the Partition ID is the same for two Beacon Key Sources, they can share the same cache entries in the cache.
114+
* @return Partition ID to distinguish Beacon Key Sources writing to a Shared cache. If the Partition ID is the same for two Beacon Key Sources, they can share the same cache entries in the Shared cache.
115115
*/
116116
String partitionId();
117117

‎TestVectors/dafny/DDBEncryption/Model/AwsCryptographyDynamoDbEncryptionTypesWrapped.dfy

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -2,10 +2,10 @@
22
// SPDX-License-Identifier: Apache-2.0
33
// Do not modify this file. This file is machine generated, and any changes to it will be overwritten.
44
include "../../../../submodules/MaterialProviders/StandardLibrary/src/Index.dfy"
5-
// BEGIN MANUAL EDIT
5+
// BEGIN MANUAL EDIT
66
include "../../../../DynamoDbEncryption/dafny/DynamoDbEncryption/src/Index.dfy"
77
include "../../../../submodules/MaterialProviders/TestVectorsAwsCryptographicMaterialProviders/dafny/KeyVectors/src/Index.dfy"
8-
// END MANUAL EDIT
8+
// END MANUAL EDIT
99
abstract module WrappedAbstractAwsCryptographyDynamoDbEncryptionService {
1010
import opened Wrappers
1111
import opened StandardLibrary.UInt

‎TestVectors/dafny/DDBEncryption/src/JsonConfig.dfy

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -526,7 +526,7 @@ module {:options "-functionSyntax:4"} JsonConfig {
526526
var client :- expect Primitives.AtomicPrimitives();
527527

528528
// Create a test partitionIdBytes
529-
var partitionIdBytes : seq<uint8> := [1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16];
529+
var partitionIdBytes : seq<uint8> :- expect SI.GeneratePartitionId();
530530
var src := SI.KeySource(client, store, SI.SingleLoc("foo"), cache, 100 as uint32, partitionIdBytes);
531531

532532
var bv :- expect SI.MakeBeaconVersion(1, src, map[], map[], map[]);

0 commit comments

Comments
 (0)
Please sign in to comment.