chore: split vc gen on some methods to migrate to Dafny 4.4

aws · Nov 28, 2023 · c17933c · c17933c
1 parent 9883933
commit c17933c
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,