Merge branch 'mainline' into jocorell/update-testvectors

aws · Nov 29, 2023 · 743c495 · 743c495
2 parents 6427c39 + fdc65ca
commit 743c495
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 2 deletions.
diff --git a/AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/MessageBody.dfy b/AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/MessageBody.dfy
@@ -653,7 +653,7 @@ module MessageBody {
     return Success(finalFrame);
   }
 
-  method DecryptFramedMessageBody(
+  method {:vcs_split_on_every_assert} DecryptFramedMessageBody(
     body: FramedMessage,
     key: seq<uint8>,
     crypto: Primitives.AtomicPrimitivesClient

diff --git a/AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/Serialize/EncryptedDataKeys.dfy b/AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/Serialize/EncryptedDataKeys.dfy
@@ -263,7 +263,7 @@ module {:options "/functionSyntax:4" } EncryptedDataKeys {
     }
   }
 
-  lemma ReadEncryptedDataKeysSectionIsComplete(
+  lemma {:vcs_split_on_every_assert} ReadEncryptedDataKeysSectionIsComplete(
     data: ESDKEncryptedDataKeys,
     bytes: seq<uint8>,
     buffer: ReadableBuffer,