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 77abfc2

Browse files
RitvikKapilaRitvikKapila
committedDec 13, 2024·
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

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

‎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

0 commit comments

Comments
 (0)
Please sign in to comment.