m

Author: ajewellamz

DynamoDbEncryption/dafny/DynamoDbEncryption/src/Beacon.dfy

@@ -149,7 +149,7 @@ module BaseBeacon {
 
     //= specification/searchable-encryption/beacons.md#beacon-constraint
     //# If an item is being written or queried as partition `X`, but the [standard beacon](#standard-beacon-initialization) is constrained to only `N` partitions,
-    //# then the partition used to [encode](#partition-beacon-encoding) the beacon MUST be `X % N`, where `%` is the modulo or remainder operation.
+    //# then the partition used to [encode](#beacon-partition-encoding) the beacon MUST be `X % N`, where `%` is the modulo or remainder operation.
     function method constrained_partition(partition : PartitionNumber) : PartitionBytes
     {
       if numberOfPartitions == 0 || partition == 0 then
@@ -169,7 +169,7 @@ module BaseBeacon {
                 && |ret.value| == (((length as uint8) + 3) / 4) as nat
     {
       //= specification/searchable-encryption/beacons.md#value-for-a-non-set-standard-beacon
-      //# - The serialized form MUST be augmented as per [partition beacon encoding](#partition-beacon-encoding).
+      //# - The serialized form MUST be augmented as per [beacon partition encoding](#beacon-partition-encoding).
       base.hash(val, key, length, constrained_partition(partition))
     }
 

DynamoDbEncryption/dafny/DynamoDbEncryption/src/Util.dfy

@@ -96,11 +96,11 @@ module DynamoDbEncryptionUtil {
 
   function method PartitionNumberToBytes(x : PartitionNumber) : PartitionBytes
   {
-    //= specification/searchable-encryption/beacons.md#partition-beacon-encoding
+    //= specification/searchable-encryption/beacons.md#beacon-partition-encoding
     //# If this number is zero, then the input sequence of bytes MUST be returned unchanged.
     if x == 0 then
       []
-    //= specification/searchable-encryption/beacons.md#partition-beacon-encoding
+    //= specification/searchable-encryption/beacons.md#beacon-partition-encoding
     //# Otherwise, a single byte with a value equal to this calculated partition number, MUST be appended to the input sequence of bytes.
     else
       [x as uint8]

specification/searchable-encryption/beacons.md

@@ -413,7 +413,7 @@ These parts may come from these locally defined parts lists, or from the
 A beacon may be constrained to fewer partitions than is specified in the [beacon version](search-config.md#beacon-version-initialization).
 
 If an item is being written or queried as partition `X`, but the [standard beacon](#standard-beacon-initialization) is constrained to only `N` partitions,
-then the partition used to [encode](#partition-beacon-encoding) the beacon MUST be `X % N`, where `%` is the modulo or remainder operation.
+then the partition used to [encode](#beacon-partition-encoding) the beacon MUST be `X % N`, where `%` is the modulo or remainder operation.
 
 Examples:
 
@@ -491,7 +491,7 @@ Both standard and compound beacons define two operations
 
 - This operation MUST convert the attribute value of the associated field to
   a sequence of bytes, as per [attribute serialization](../dynamodb-encryption-client/ddb-attribute-serialization.md).
-- The serialized form MUST be augmented as per [beacon partition encoding](#partition-beacon-encoding).
+- The serialized form MUST be augmented as per [beacon partition encoding](#beacon-partition-encoding).
 - This operation MUST return the [basicHash](#basichash) of the resulting bytes and the configured [beacon length](#beacon-length).
 - The returned
   [AttributeValue](https://docs.aws.amazon.com/amazondynamodb/latest/APIReference/API_AttributeValue.html)