m

aws · Oct 31, 2024 · b11dc2e · b11dc2e
1 parent f945592
commit b11dc2e
Show file tree

Hide file tree

Showing 4 changed files with 10 additions and 10 deletions.
diff --git a/.github/workflows/library_format.yml b/.github/workflows/library_format.yml
@@ -39,7 +39,7 @@ jobs:
       - name: Setup Dafny
         uses: dafny-lang/[email protected]
         with:
-          dafny-version: ${{ '4.2.0' }}
+          dafny-version: ${{ inputs.dafny }}
 
       - name: Check format of Java code et al
         run: |

diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/SearchInfo.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/SearchInfo.dfy
@@ -71,11 +71,11 @@ module SearchableEncryptionInfo {
       //# MUST be generated in accordance with [HMAC Key Generation](#hmac-key-generation).
       var newKey :- GetBeaconKey(client, key, keysLeft[0]);
       reveal Seq.HasNoDuplicates();
-      //= specification/searchable-encryption/search-config.md#get-beacon-key-materials
-      //# [Beacon Key Materials](../../submodules/MaterialProviders/aws-encryption-sdk-specification/framework/structures.md#beacon-key-materials) MUST be generated
-      //# with the [beacon key id](#beacon-key-id) equal to the `beacon key id`
-      //# and the [HMAC Keys](../../submodules/MaterialProviders/aws-encryption-sdk-specification/framework/structures.md#hmac-keys) equal to a map
-      //# of every [standard beacons](beacons.md#standard-beacon-initialization) name to its generated HMAC key.
+             //= specification/searchable-encryption/search-config.md#get-beacon-key-materials
+             //# [Beacon Key Materials](../../submodules/MaterialProviders/aws-encryption-sdk-specification/framework/structures.md#beacon-key-materials) MUST be generated
+             //# with the [beacon key id](#beacon-key-id) equal to the `beacon key id`
+             //# and the [HMAC Keys](../../submodules/MaterialProviders/aws-encryption-sdk-specification/framework/structures.md#hmac-keys) equal to a map
+             //# of every [standard beacons](beacons.md#standard-beacon-initialization) name to its generated HMAC key.
       output := GetHmacKeys(client, allKeys, keysLeft[1..], key, acc[keysLeft[0] := newKey]);
     }
   }

diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/test/BeaconTestFixtures.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/test/BeaconTestFixtures.dfy
@@ -182,8 +182,8 @@ module BeaconTestFixtures {
     ensures fresh(output.keyStore.Modifies)
     ensures output.version == 1
     ensures
-    && output.keySource.multi?
-    && output.keySource.multi.cache.None?
+      && output.keySource.multi?
+      && output.keySource.multi.cache.None?
   {
     var store := GetKeyStore();
     return BeaconVersion (

diff --git a/DynamoDbEncryption/dafny/StructuredEncryption/src/Header.dfy b/DynamoDbEncryption/dafny/StructuredEncryption/src/Header.dfy
@@ -132,7 +132,7 @@ module StructuredEncryptionHeader {
                     + SerializeLegend(legend)
                     + SerializeContext(encContext)
                     + SerializeDataKeys(dataKeys)
-                    )
+                  )
     {
       var context := SerializeContext(encContext);
       var keys := SerializeDataKeys(dataKeys);
@@ -630,7 +630,7 @@ module StructuredEncryptionHeader {
                   + k.keyProviderInfo
                   + UInt16ToSeq(cipherSize)
                   + k.ciphertext
-                  )
+                )
   {
     UInt16ToSeq(|k.keyProviderId| as uint16)
     + k.keyProviderId