From ccb37b7075ad1b22d4bb9a8dfee569f57c1b4640 Mon Sep 17 00:00:00 2001 From: Jay Lorch Date: Tue, 16 Nov 2021 18:50:49 -0800 Subject: [PATCH] Support for Dafny 3.3.0 --- ironfleet/README.md | 2 +- .../Impl/Common/GenericMarshalling.i.dfy | 3 ++- .../Distributed/Impl/RSL/ElectionModel.i.dfy | 2 +- .../SHT/RefinementProof/RefinementProof.i.dfy | 4 ++-- .../Distributed/Services/SHT/Marshall.i.dfy | 20 ++++++++++++++----- ironfleet/src/Dafny/Libraries/Math/div.i.dfy | 18 +++++++++++++++-- 6 files changed, 37 insertions(+), 12 deletions(-) diff --git a/ironfleet/README.md b/ironfleet/README.md index 482d2d80..e829229e 100755 --- a/ironfleet/README.md +++ b/ironfleet/README.md @@ -37,7 +37,7 @@ IronFleet is licensed under the MIT license included in the [LICENSE](./LICENSE) To use Ironfleet, you'll need the following tools: * .NET 5.0 SDK (available at `https://dotnet.microsoft.com/download`) - * Dafny v3.2.0 (verifier, available at `https://github.com/dafny-lang/dafny`) + * Dafny v3.3.0 (verifier, available at `https://github.com/dafny-lang/dafny`) * python 2 or 3 (needed for running scons) * scons (installable by running `pip install scons`) diff --git a/ironfleet/src/Dafny/Distributed/Impl/Common/GenericMarshalling.i.dfy b/ironfleet/src/Dafny/Distributed/Impl/Common/GenericMarshalling.i.dfy index 9d715dd7..662ef8b6 100755 --- a/ironfleet/src/Dafny/Distributed/Impl/Common/GenericMarshalling.i.dfy +++ b/ironfleet/src/Dafny/Distributed/Impl/Common/GenericMarshalling.i.dfy @@ -85,6 +85,7 @@ predicate Trigger(i:int) function method parse_Uint64(data:seq) : (Option, seq) requires |data| < 0x1_0000_0000_0000_0000 + ensures if |data| >= 8 then |parse_Uint64(data).1| == |data| - 8 else |parse_Uint64(data).1| == 0 { if |data| as uint64 >= Uint64Size() then (Some(VUint64(SeqByteToUint64(data[..Uint64Size()]))), data[Uint64Size()..]) @@ -1718,7 +1719,7 @@ method MarshallByteArray(val:V, grammar:G, data:array, index:uint64) retur ghost var len := tuple.0; ghost var rest := tuple.1; assert{:split_here} true; - // assert len.v.u == |val.b| as uint64; + assert len.v.u == |val.b| as uint64; assert rest == data[index + 8..(index as int) + SizeOfV(val)] == val.b; assert !len.None? && (len.v.u as int) <= |rest|; diff --git a/ironfleet/src/Dafny/Distributed/Impl/RSL/ElectionModel.i.dfy b/ironfleet/src/Dafny/Distributed/Impl/RSL/ElectionModel.i.dfy index c74f0569..37b68216 100755 --- a/ironfleet/src/Dafny/Distributed/Impl/RSL/ElectionModel.i.dfy +++ b/ironfleet/src/Dafny/Distributed/Impl/RSL/ElectionModel.i.dfy @@ -96,7 +96,7 @@ lemma lemma_BoundCRequestSequence(s:seq, lengthBound:uint64) { } -ghost method FindMatchingRequest(s:seq, headers:set, header:CRequestHeader) returns (index:int) +lemma FindMatchingRequest(s:seq, headers:set, header:CRequestHeader) returns (index:int) requires HeadersMatch(s, headers) requires header in headers requires |s| >= 1 diff --git a/ironfleet/src/Dafny/Distributed/Protocol/SHT/RefinementProof/RefinementProof.i.dfy b/ironfleet/src/Dafny/Distributed/Protocol/SHT/RefinementProof/RefinementProof.i.dfy index 6f7ccb26..8a78b8c4 100755 --- a/ironfleet/src/Dafny/Distributed/Protocol/SHT/RefinementProof/RefinementProof.i.dfy +++ b/ironfleet/src/Dafny/Distributed/Protocol/SHT/RefinementProof/RefinementProof.i.dfy @@ -66,7 +66,7 @@ lemma HostClaimsKey_forces_FindHashTable(s:SHT_State, id:NodeIdentity, k:Key) } -ghost method UniquePacketClaimsKey_forces_FindHashTable(s:SHT_State, k:Key) returns (pkt:Packet) +lemma UniquePacketClaimsKey_forces_FindHashTable(s:SHT_State, k:Key) returns (pkt:Packet) requires MapComplete(s); requires PacketsHaveSaneHeaders(s); requires AllDelegationsToKnownHosts(s); @@ -82,7 +82,7 @@ ghost method UniquePacketClaimsKey_forces_FindHashTable(s:SHT_State, k:Key) retu } -ghost method HostClaimsKey_forces_FindHostHashTable(s:SHT_State, k:Key) returns (id:NodeIdentity) +lemma HostClaimsKey_forces_FindHostHashTable(s:SHT_State, k:Key) returns (id:NodeIdentity) requires Inv(s); requires UniqueHostClaimsKey(s, k); ensures id in AllHostIdentities(s); diff --git a/ironfleet/src/Dafny/Distributed/Services/SHT/Marshall.i.dfy b/ironfleet/src/Dafny/Distributed/Services/SHT/Marshall.i.dfy index 910d8c6c..0777c0d4 100755 --- a/ironfleet/src/Dafny/Distributed/Services/SHT/Marshall.i.dfy +++ b/ironfleet/src/Dafny/Distributed/Services/SHT/Marshall.i.dfy @@ -52,8 +52,8 @@ module MarshallProof_i { ensures caseId == parse_Uint64(data).0.v.u; ensures 0 <= caseId as int < |g.cases|; ensures rest == parse_Uint64(data).1; - ensures parse_Val(rest, g.cases[caseId]).0.Some?; - ensures val == parse_Val(rest, g.cases[caseId]).0.v + ensures parse_Val(rest, g.cases[caseId]).0.Some?; + ensures val == parse_Val(rest, g.cases[caseId]).0.v; ensures v == VCase(caseId, val); ensures ValInGrammar(val, g.cases[caseId]); ensures parse_Val(data, g) == parse_Case(data, g.cases) @@ -404,7 +404,7 @@ module MarshallProof_i { } } - lemma {:fuel ValInGrammar,5} {:timeLimitMultiplier 4} lemma_ParseMarshallReply(bytes:seq, reply:AppReply, msg:SingleMessage, reserved_bytes:seq) + lemma {:fuel ValInGrammar,5} {:timeLimitMultiplier 5} lemma_ParseMarshallReply(bytes:seq, reply:AppReply, msg:SingleMessage, reserved_bytes:seq) requires CSingleMessageIsAbstractable(SHTDemarshallData(bytes)); requires AbstractifyCSingleMessageToSingleMessage(SHTDemarshallData(bytes)) == msg; requires CSingleMessageMarshallable(SHTDemarshallData(bytes)); @@ -484,8 +484,13 @@ module MarshallProof_i { assert len_dst == SeqByteToUint64(rest1[..8]) == SeqByteToUint64(data[16..24]) == |reserved_bytes| as uint64; assert len_dst as int == |reserved_bytes|; - assert val_dst.b == rest1[8 .. 8 + len_dst]; - assert val_dst.b == data[24 .. 24 + len_dst] == reserved_bytes; + calc { + val_dst.b; + rest1[8 .. 8 + len_dst]; + data[16..][8 .. 8 + len_dst]; + data[24 .. 24 + len_dst]; + reserved_bytes; + } assert rest2[..8] == data[24 + len_dst .. 32 + len_dst] == [0, 0, 0, 0, 0, 0, 0, 2]; assert mCaseId == 2; @@ -527,6 +532,11 @@ module MarshallProof_i { // Handle the two subcases of OptionalValue if reply.ov.ValuePresent? { assert rest4[..8] == [ 0, 0, 0, 0, 0, 0, 0, 0]; + + assert rest5 == parse_Uint64(rest4).1; + assert |rest5| == |rest4| - 8; + assert |rest5| < 0x1_0000_0000_0000_0000; + var byteLen, bytesVal, rest6 := lemma_ParseValCorrectVByteArray(rest5, valCaseVal, GByteArray); calc { byteLen; diff --git a/ironfleet/src/Dafny/Libraries/Math/div.i.dfy b/ironfleet/src/Dafny/Libraries/Math/div.i.dfy index 896ae99e..1aee7bca 100755 --- a/ironfleet/src/Dafny/Libraries/Math/div.i.dfy +++ b/ironfleet/src/Dafny/Libraries/Math/div.i.dfy @@ -318,7 +318,7 @@ lemma {:timeLimitMultiplier 2} lemma_mod_neg_neg(x:int, d:int) lemma_mul_auto(); } -lemma {:timeLimitMultiplier 2} lemma_fundamental_div_mod_converse(x:int, d:int, q:int, r:int) +lemma lemma_fundamental_div_mod_converse(x:int, d:int, q:int, r:int) requires d != 0 requires 0 <= r < d requires x == q * d + r @@ -326,7 +326,21 @@ lemma {:timeLimitMultiplier 2} lemma_fundamental_div_mod_converse(x:int, d:int, ensures r == x%d { lemma_div_auto(d); - lemma_mul_auto_induction(q, u => u == (u * d + r) / d); + + var f := u => u == (u * d + r) / d; + forall i {:trigger TMulAutoLe(0, i)} | TMulAutoLe(0, i) && f(i) + ensures f(i + 1) + { + calc { + ((i + 1) * d + r) / d; + { lemma_mul_is_distributive_add_other_way(d, i, 1); } + (i * d + 1 * d + r) / d; + (i * d + d + r) / d; + (i * d + r) / d + 1; + i + 1; + } + } + lemma_mul_auto_induction(q, f); lemma_mul_auto_induction(q, u => r == (u * d + r) % d); // REVIEW: this is a plausible alternative, but it times out: