Skip to content

Commit 9f84eb9

Browse files
RitvikKapilaRitvikKapila
committed
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)

0 commit comments

Comments
 (0)