From 9f9276067bce64c41686f796704df217c40a7498 Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Mon, 22 Jan 2024 13:24:59 -0800 Subject: [PATCH 1/3] Update one definition to prove with Dafny 4.4 --- .../dafny/AwsEncryptionSdk/src/MessageBody.dfy | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) diff --git a/AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/MessageBody.dfy b/AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/MessageBody.dfy index a72e05137..a7009ac89 100644 --- a/AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/MessageBody.dfy +++ b/AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/MessageBody.dfy @@ -974,7 +974,6 @@ module MessageBody { ==> && res.value.data.finalFrame.header == header { - reveal CorrectlyReadRange(); var sequenceNumber :- ReadUInt32(continuation); //= compliance/client-apis/decrypt.txt#2.7.4 @@ -1034,6 +1033,12 @@ module MessageBody { assert CorrectlyRead(buffer, Success(SuccessfulRead(nextRegularFrames, regularFrame.tail)), WriteMessageRegularFrames) by { reveal CorrectlyReadRange(); } + assert buffer.start <= regularFrame.tail.start by { + reveal CorrectlyReadRange(); + } + assert CorrectlyReadRange(buffer, regularFrame.tail, buffer.bytes[buffer.start..regularFrame.tail.start]) by { + reveal CorrectlyReadRange(); + } ReadFramedMessageBody( buffer, @@ -1069,6 +1074,9 @@ module MessageBody { assert {:split_here} true; assert CorrectlyRead(continuation, Success(finalFrame), Frames.WriteFinalFrame); assert {:split_here} true; + assert CorrectlyRead(buffer, Success(SuccessfulRead(body, finalFrame.tail)), WriteFramedMessageBody) by { + reveal CorrectlyReadRange(); + } Success(SuccessfulRead(body, finalFrame.tail)) } From 2407f7ed37f425bdfc4b9165d1a1c1cef42fea1b Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Wed, 24 Jan 2024 13:43:58 -0800 Subject: [PATCH 2/3] Reduce resource use with Dafny 4.2.0 Also helps and works with Dafny 4.3.0 and 4.4.0. --- AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/MessageBody.dfy | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/MessageBody.dfy b/AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/MessageBody.dfy index a7009ac89..a74b014f4 100644 --- a/AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/MessageBody.dfy +++ b/AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/MessageBody.dfy @@ -1063,8 +1063,6 @@ module MessageBody { ); assert {:split_here} true; - assert MessageFramesAreMonotonic(regularFrames + [finalFrame.data]); - assert MessageFramesAreForTheSameMessage(regularFrames + [finalFrame.data]); var body: FramedMessage := FramedMessageBody( regularFrames := regularFrames, @@ -1075,6 +1073,8 @@ module MessageBody { assert CorrectlyRead(continuation, Success(finalFrame), Frames.WriteFinalFrame); assert {:split_here} true; assert CorrectlyRead(buffer, Success(SuccessfulRead(body, finalFrame.tail)), WriteFramedMessageBody) by { + assert MessageFramesAreMonotonic(regularFrames + [finalFrame.data]); + assert MessageFramesAreForTheSameMessage(regularFrames + [finalFrame.data]); reveal CorrectlyReadRange(); } Success(SuccessfulRead(body, finalFrame.tail)) From 24ddf9a7b2840bea4a37c633c45d60cdfc177184 Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Mon, 29 Jan 2024 09:56:07 -0800 Subject: [PATCH 3/3] Bump mpl submodule --- mpl | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/mpl b/mpl index cce342923..ccf9727aa 160000 --- a/mpl +++ b/mpl @@ -1 +1 @@ -Subproject commit cce342923ce5602f2e6162dccca44ecefaffca68 +Subproject commit ccf9727aad8994a2ec62c659be5fa91bb4c98d5a