Skip to content

Commit 77abfc2

Browse files
RitvikKapilaRitvikKapila
committed
m
1 parent 9f84eb9 commit 77abfc2

20 files changed

+134
-134
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/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: 18 additions & 18 deletions
Original file line numberDiff line numberDiff line change
@@ -504,10 +504,10 @@ module SearchConfigToInfo {
504504
//= type=implication
505505
//# Initialization MUST fail if two standard beacons are configured with the same location.
506506
&& FindBeaconWithThisLocation(converted, loc).None?
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.
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.
511511
&& FindVirtualFieldWithThisLocation(virtualFields, {loc}).None?
512512
{
513513
if |beacons| == 0 {
@@ -636,10 +636,10 @@ module SearchConfigToInfo {
636636
//# or is not `signed`.
637637
ensures
638638
(&& 0 < |parts|
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).
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).
643643
&& GetLoc(parts[0].name, parts[0].loc).Success?
644644
&& var loc := GetLoc(parts[0].name, parts[0].loc).value;
645645
&& !IsSignOnly(outer, CB.Signed(parts[0].prefix, parts[0].name, loc).loc))
@@ -721,10 +721,10 @@ module SearchConfigToInfo {
721721
ensures ret.Success? ==>
722722
&& |ret.value| == 1
723723
&& |ret.value[0].parts| == |parts| + |converted|
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.
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.
728728
&& CB.OrderedParts(allParts, numNon)
729729
&& (forall i | 0 <= i < |ret.value[0].parts| ::
730730
&& ret.value[0].parts[i].part == allParts[i]
@@ -1109,14 +1109,14 @@ module SearchConfigToInfo {
11091109
ensures ret.Success? && 0 < |names| && data[names[0]].Standard? && data[names[0]].std.share.Some? ==>
11101110
&& var share := data[names[0]].std.share.value;
11111111
&& IsValidShare(data, names[0], data[names[0]].std.length, share).Success?
1112-
//= specification/searchable-encryption/beacons.md#shared-initialization
1113-
//= type=implication
1114-
//# 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.
11151115
&& share in data
11161116
&& data[share].Standard?
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).
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).
11201120
&& data[share].std.length == data[names[0]].std.length
11211121
{
11221122
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: 17 additions & 17 deletions
Original file line numberDiff line numberDiff line change
@@ -73,11 +73,11 @@ module SearchableEncryptionInfo {
7373
//# MUST be generated in accordance with [HMAC Key Generation](#hmac-key-generation).
7474
var newKey :- GetBeaconKey(client, key, keysLeft[0]);
7575
reveal Seq.HasNoDuplicates();
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.
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.
8181
output := GetHmacKeys(client, allKeys, keysLeft[1..], key, acc[keysLeft[0] := newKey]);
8282
}
8383
}
@@ -107,14 +107,14 @@ module SearchableEncryptionInfo {
107107
&& hkdfInput.digestAlgorithm == Prim.SHA_512
108108
&& hkdfInput.salt == None
109109
&& hkdfInput.ikm == key
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.
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.
114114
&& hkdfInput.info == info
115-
//= specification/searchable-encryption/search-config.md#hmac-key-generation
116-
//= type=implication
117-
//# 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.
118118
&& hkdfInput.expectedLength == 64
119119
{
120120
var info :- UTF8.Encode("AWS_DBE_SCAN_BEACON" + name).MapFailure(e => E(e));
@@ -234,8 +234,8 @@ module SearchableEncryptionInfo {
234234
&& var cacheInput := Seq.Last(newHistory).input;
235235
&& var cacheOutput := Seq.Last(newHistory).output;
236236
&& UTF8.Encode(keyId).Success?
237-
// TODO - why is this verifying?
238-
&& cacheInput.identifier == UTF8.Encode(keyId).value
237+
// TODO - why is this verifying?
238+
&& cacheInput.identifier == RESOURCE_ID_HIERARCHICAL_KEYRING + NULL_BYTE + SCOPE_ID_SEARCHABLE_ENCRYPTION + NULL_BYTE + partitionIdBytes + NULL_BYTE + UTF8.Encode(keyId).value
239239

240240
//= specification/searchable-encryption/search-config.md#get-beacon-key-materials
241241
//= type=implication
@@ -250,9 +250,9 @@ module SearchableEncryptionInfo {
250250
&& var oldGetHistory := old(store.History.GetBeaconKey);
251251
&& var newGetHistory := store.History.GetBeaconKey;
252252
&& |newGetHistory| == |oldGetHistory|+1
253-
//= specification/searchable-encryption/search-config.md#get-beacon-key-materials
254-
//= type=implication
255-
//# 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.
256256
&& Seq.Last(newGetHistory).output.Success?
257257
&& var storeInput := Seq.Last(newGetHistory).input;
258258
&& var storeOutput := Seq.Last(newGetHistory).output;

‎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/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

0 commit comments

Comments
 (0)