Support for Dafny 3.3.0

secure-foundations · Nov 17, 2021 · ccb37b7 · ccb37b7
1 parent e2bf4a2
commit ccb37b7
Show file tree

Hide file tree

Showing 6 changed files with 37 additions and 12 deletions.
diff --git 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
@@ -85,6 +85,7 @@ predicate Trigger(i:int)
 
 function method parse_Uint64(data:seq<byte>) : (Option<V>, seq<byte>)
   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<byte>, 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
@@ -96,7 +96,7 @@ lemma lemma_BoundCRequestSequence(s:seq<CRequest>, lengthBound:uint64)
 {
 }
 
-ghost method FindMatchingRequest(s:seq<CRequest>, headers:set<CRequestHeader>, header:CRequestHeader) returns (index:int)
+lemma FindMatchingRequest(s:seq<CRequest>, headers:set<CRequestHeader>, 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
@@ -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
@@ -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<byte>, reply:AppReply, msg:SingleMessage<Message>, reserved_bytes:seq<byte>) 
+    lemma {:fuel ValInGrammar,5} {:timeLimitMultiplier 5} lemma_ParseMarshallReply(bytes:seq<byte>, reply:AppReply, msg:SingleMessage<Message>, reserved_bytes:seq<byte>) 
         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
@@ -318,15 +318,29 @@ 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
   ensures q == x/d
   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: