update

Author: RitvikKapila

DynamoDbEncryption/dafny/DynamoDbEncryption/test/Beacon.dfy

@@ -273,6 +273,9 @@ module TestBaseBeacon {
     var badVersion := GetLotsaBeaconsMultiWithSharedCacheWithBadKeyStore(cache := sharedCache, partitionId := Some(partitionIdBadVersion));
     var badSrc :- expect C.MakeKeySource(FullTableConfig, badVersion.keyStore, badVersion.keySource, primitives);
     var badBv :- expect C.ConvertVersionWithSource(FullTableConfig, badVersion, badSrc);
+    // This KeyId is a valid branch_key_id present in the KeyStoreDdbTable.
+    // Providing a valid branch_key_id is important in this method because unlike other tests in Beacon.dfy,
+    // this is used in a test which actually fetches data from DynamoDb without using a Literal KeySource.
     var badAttrs := badBv.GenerateEncryptedBeacons(SimpleItem, KeyId("040a32a8-3737-4f16-a3ba-bd4449556d73"));
     expect badAttrs.Failure?;
 
@@ -309,6 +312,9 @@ module TestBaseBeacon {
     var badVersion := GetLotsaBeaconsMultiWithSharedCacheWithBadKeyStore(cache := sharedCache, partitionId := None);
     var badSrc :- expect C.MakeKeySource(FullTableConfig, badVersion.keyStore, badVersion.keySource, primitives);
     var badBv :- expect C.ConvertVersionWithSource(FullTableConfig, badVersion, badSrc);
+    // This KeyId is a valid branch_key_id present in the KeyStoreDdbTable.
+    // Providing a valid branch_key_id is important in this method because unlike other tests in Beacon.dfy,
+    // this is used in a test which actually fetches data from DynamoDb without using a Literal KeySource.
     var badAttrs := badBv.GenerateEncryptedBeacons(SimpleItem, KeyId("040a32a8-3737-4f16-a3ba-bd4449556d73"));
     expect badAttrs.Failure?;
 

DynamoDbEncryption/dafny/DynamoDbEncryption/test/BeaconTestFixtures.dfy

@@ -151,17 +151,18 @@ module BeaconTestFixtures {
   {
     var kmsClient :- expect KMS.KMSClient();
     var ddbClient :- expect DDBC.DynamoDBClient();
+    // This is the bad-arn key which does NOT exist.
     var kmsConfig := KTypes.KMSConfiguration.kmsKeyArn(
       "arn:aws:kms:us-west-2:370957321024:key/bad-arn"
     );
     var keyStoreConfig := KTypes.KeyStoreConfig(
       id := None,
       kmsConfiguration := kmsConfig,
       // This needs to be the same as logicalKeyStoreName of KeyStore
-      // generated by GetKeyStore to have the same cache identifier
+      // generated by GetKeyStore to have the same cache identifier.
       logicalKeyStoreName := "KeyStoreDdbTable",
       grantTokens := None,
-      // This is the bad-table-name which does NOT exist
+      // This is the bad-table-name which does NOT exist.
       ddbTableName := "bad-table-name",
       ddbClient := Some(ddbClient),
       kmsClient := Some(kmsClient)
@@ -241,9 +242,9 @@ module BeaconTestFixtures {
     return BeaconVersion (
         version := 1,
         keyStore := store,
-        // This KeyId is a valid branch_key_id present in the KeyStoreDdbTable
+        // This KeyId is a valid branch_key_id present in the KeyStoreDdbTable.
         // Providing a valid branch_key_id is important in this method because unlike other tests in Beacon.dfy,
-        // this is used in a test which actually fetches data from DynamoDb without using a Literal KeySource
+        // this is used in a test which actually fetches data from DynamoDb without using a Literal KeySource.
         keySource := single(SingleKeyStore(keyId := "040a32a8-3737-4f16-a3ba-bd4449556d73", cacheTTL := 42, cache := Some(cache), partitionId := partitionId)),
         standardBeacons := [std2, std4, std6, NameTitleBeacon, NameB, TitleB],
         compoundBeacons := Some([NameTitle, YearName, Mixed, JustSigned]),
@@ -265,7 +266,7 @@ module BeaconTestFixtures {
     return BeaconVersion (
         version := 1,
         keyStore := store,
-        // This KeyId is a valid branch_key_id present in the KeyStoreDdbTable
+        // This KeyId is a valid branch_key_id present in the KeyStoreDdbTable.
         // Providing a valid branch_key_id is important in this method because unlike other tests in Beacon.dfy,
         // this is used in a test which actually fetches data from DynamoDb without using a Literal KeySource.
         // Even though this method creates a BeaconVersion with a Bad Key Store which does NOT exist,