Skip to content

chore(dafny-verification): fix timeout for Dafny 4.8.1 #690

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
RitvikKapila merged 2 commits into from
Oct 30, 2024
Merged

chore(dafny-verification): fix timeout for Dafny 4.8.1 #690

Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
bb592e0
chore(dafny-verification): fix timeout for Dafny 4.8.1
RitvikKapila Oct 23, 2024
3426484
update
RitvikKapila Oct 27, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
81 changes: 41 additions & 40 deletions AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/MessageBody.dfy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -964,17 +964,16 @@ module MessageBody {
:(res: ReadCorrect<FramedMessage>)
requires forall frame: Frames.Frame | frame in regularFrames :: frame.header == header
requires buffer.bytes == continuation.bytes
requires buffer.start <= continuation.start
requires buffer.start <= continuation.start
requires 0 <= continuation.start <= |buffer.bytes|
requires CorrectlyReadRange(buffer, continuation, buffer.bytes[buffer.start..continuation.start])
requires CorrectlyRead(buffer, Success(SuccessfulRead(regularFrames, continuation)), WriteMessageRegularFrames)
decreases ENDFRAME_SEQUENCE_NUMBER as nat - |regularFrames|
ensures CorrectlyRead(buffer, res, WriteFramedMessageBody)
ensures res.Success?
==>
&& res.value.data.finalFrame.header == header
==>
&& res.value.data.finalFrame.header == header
{
reveal CorrectlyReadRange();
var sequenceNumber :- ReadUInt32(continuation);

//= compliance/client-apis/decrypt.txt#2.7.4
Expand All @@ -984,19 +983,14 @@ module MessageBody {
//# (../data-format/message-body.md#final-frame) or regular frame
//# (../fata-format/message-body/md#regular-frame).
if (sequenceNumber.data != ENDFRAME_SEQUENCE_NUMBER) then

assert {:split_here} true;

//= compliance/client-apis/decrypt.txt#2.7.4
//# Otherwise, this MUST
//# be deserialized as the sequence number (../data-format/message-
//# header.md#sequence-number) and the following bytes according to the
//# regular frame spec (../data-format/message-body.md#regular-frame).
var regularFrame :- Frames.ReadRegularFrame(continuation, header);
assert buffer.bytes == continuation.bytes;
assert buffer.bytes == regularFrame.tail.bytes by {
reveal CorrectlyReadRange();
}

//= compliance/client-apis/decrypt.txt#2.7.4
//# If this is framed data and the first
//# frame sequentially, this value MUST be 1.
Expand All @@ -1008,19 +1002,15 @@ module MessageBody {
//# of the previous frame.
:- Need(regularFrame.data.seqNum as nat == |regularFrames| + 1, Error("Sequence number out of order."));

assert {:split_here} true;
LemmaAddingNextRegularFrame(regularFrames, regularFrame.data);

var nextRegularFrames: MessageRegularFrames := regularFrames + [regularFrame.data];

assert {:split_here} true;
assert CorrectlyRead(continuation, Success(regularFrame), Frames.WriteRegularFrame);
assert continuation.bytes == regularFrame.tail.bytes by {
CorrectlyReadByteRange(buffer, continuation, WriteMessageRegularFrames(regularFrames));
AppendToCorrectlyReadByteRange(buffer, continuation, regularFrame.tail, Frames.WriteRegularFrame(regularFrame.data));
assert buffer.bytes == continuation.bytes == regularFrame.tail.bytes by {
reveal CorrectlyReadRange();
}

assert {:split_here} true;

// This method recursively reads all the frames in the buffer,
// instead of reading one frame a time, so this requirement cannot be met
//= compliance/client-apis/decrypt.txt#2.7.4
Expand All @@ -1031,17 +1021,20 @@ module MessageBody {
//# (../framework/algorithm-suites.md#encryption-algorithm) specified by
//# the algorithm suite (../framework/algorithm-suites.md), with the
//# following inputs:
var res := Success(SuccessfulRead(nextRegularFrames, regularFrame.tail));
assert CorrectlyRead(buffer, res, WriteMessageRegularFrames) by {
reveal CorrectlyReadRange();

var tail := res.value.tail;
var readRange := WriteMessageRegularFrames(res.value.data);
assert buffer.bytes == tail.bytes;
assert buffer.start <= tail.start <= |buffer.bytes|;
assert buffer.bytes[buffer.start..] == tail.bytes[buffer.start..];
assert readRange <= buffer.bytes[buffer.start..];
assert tail.start == buffer.start + |readRange|;
assert CorrectlyRead(
buffer,
Success(SuccessfulRead(nextRegularFrames, regularFrame.tail)),
WriteMessageRegularFrames
) by {
calc {
buffer.bytes[buffer.start..continuation.start] + Frames.WriteRegularFrame(regularFrame.data);
== {CorrectlyReadByteRange(buffer, continuation, WriteMessageRegularFrames(regularFrames));}
WriteMessageRegularFrames(regularFrames) + Frames.WriteRegularFrame(regularFrame.data);
== // By definition of WriteMessageRegularFrames
WriteMessageRegularFrames(regularFrames + [regularFrame.data]);
== {assert nextRegularFrames == regularFrames + [regularFrame.data];}
WriteMessageRegularFrames(nextRegularFrames);
}
}

ReadFramedMessageBody(
Expand All @@ -1058,26 +1051,34 @@ module MessageBody {
//# number-end) and the following bytes according to the final frame spec
//# (../data-format/message-body.md#final-frame).
assert sequenceNumber.data == ENDFRAME_SEQUENCE_NUMBER;

assert {:split_here} true;

var finalFrame :- Frames.ReadFinalFrame(continuation, header);
:- Need(
finalFrame.data.seqNum as nat == |regularFrames| + 1,
Error("Sequence number out of order.")
);
finalFrame.data.seqNum as nat == |regularFrames| + 1,
Error("Sequence number out of order.")
);

assert {:split_here} true;
assert MessageFramesAreMonotonic(regularFrames + [finalFrame.data]);
assert MessageFramesAreForTheSameMessage(regularFrames + [finalFrame.data]);

var body: FramedMessage := FramedMessageBody(
regularFrames := regularFrames,
finalFrame := finalFrame.data
);
regularFrames := regularFrames,
finalFrame := finalFrame.data
);

assert CorrectlyRead(buffer, Success(SuccessfulRead(body, finalFrame.tail)), WriteFramedMessageBody) by {
AppendToCorrectlyReadByteRange(buffer, continuation, finalFrame.tail, Frames.WriteFinalFrame(finalFrame.data));
calc {
buffer.bytes[buffer.start..finalFrame.tail.start];
==
buffer.bytes[buffer.start..continuation.start] + Frames.WriteFinalFrame(finalFrame.data);
== {CorrectlyReadByteRange(buffer, continuation, WriteMessageRegularFrames(regularFrames));}
WriteMessageRegularFrames(regularFrames) + Frames.WriteFinalFrame(finalFrame.data);
== // By definition of WriteMessageRegularFrames
WriteFramedMessageBody(body);
}
}

assert {:split_here} true;
assert CorrectlyRead(continuation, Success(finalFrame), Frames.WriteFinalFrame);
assert {:split_here} true;
Success(SuccessfulRead(body, finalFrame.tail))
}

Expand Down