Update Dafny to version 4.1.0

.github/workflows/ci.yaml

@@ -20,8 +20,8 @@ jobs:
       - uses: actions/checkout@v3
       - name: install danfy
         run: |
-          wget -q https://github.com/dafny-lang/dafny/releases/download/v3.6.0/dafny-3.6.0-x64-ubuntu-16.04.zip
-          unzip -qq dafny-3.6.0-x64-ubuntu-16.04.zip
+          wget -q https://github.com/dafny-lang/dafny/releases/download/v4.1.0/dafny-4.1.0-x64-ubuntu-20.04.zip
+          unzip -qq dafny-4.1.0-x64-ubuntu-20.04.zip
           echo "dafny=$PWD/dafny/dafny" >> $GITHUB_ENV
       - name: test
         env:

count.dfy

@@ -1,4 +1,4 @@
-function count_eq<T>(x: T, s: seq<T>): nat
+function count_eq<T(==)>(x: T, s: seq<T>): nat
 {
   if s == [] then
     0
@@ -24,27 +24,27 @@ lemma count_multiset<T>(x: T, s: seq<T>)
 {
   if s == [] {
   }
-/*  
-  else if x == s[0] {
-    calc {
-      count_eq(x, s);
-      1 + count_eq(x, s[1..]);
-      multiset{s[0]}[x] + count_eq(x, s[1..]);
-      multiset{s[0]}[x] + multiset(s[1..])[x];
-      multiset([s[0]] + s[1..])[x];
-      { assert s == [s[0]] + s[1..]; }
-      multiset(s)[x];
-    }
-  } 
-*/
+  /*  
+    else if x == s[0] {
+      calc {
+        count_eq(x, s);
+        1 + count_eq(x, s[1..]);
+        multiset{s[0]}[x] + count_eq(x, s[1..]);
+        multiset{s[0]}[x] + multiset(s[1..])[x];
+        multiset([s[0]] + s[1..])[x];
+        { assert s == [s[0]] + s[1..]; }
+        multiset(s)[x];
+      }
+    } 
+  */
   else {
     assert s == [s[0]] + s[1..];
-//    calc {
-//      count_eq(x, s);
-//      (if x == s[0] then 1 else 0) + count_eq(x, s[1..]);
-//      multiset{s[0]}[x] + multiset(s[1..])[x];
-//      { assert s == [s[0]] + s[1..]; }
-//      multiset(s)[x];
-//    }
+    //    calc {
+    //      count_eq(x, s);
+    //      (if x == s[0] then 1 else 0) + count_eq(x, s[1..]);
+    //      multiset{s[0]}[x] + multiset(s[1..])[x];
+    //      { assert s == [s[0]] + s[1..]; }
+    //      multiset(s)[x];
+    //    }
   }
 }

getAllShuffledDataEntriesWithAvoidSet.dfy

@@ -15,7 +15,7 @@ method swap<T>(a: array<T>, i: int, j: int)
   a[j] := t;
 }
 
-predicate uniq<T>(s: seq<T>)
+predicate uniq<T(==)>(s: seq<T>)
 {
   forall x :: x in s ==> multiset(s)[x] == 1
 }
@@ -117,26 +117,26 @@ method getAllShuffledDataEntriesWithAvoidSet<T(==, 0)>(m_workList: array<T>, avo
   }
 
   if n > 0 {
-//    assert j == k + 1;
-//    assert forall i :: k < i < result.Length ==> result[i] in avoidSet;
-//    assert forall i :: 0 <= i <= k ==> result[i] !in avoidSet;
+    //    assert j == k + 1;
+    //    assert forall i :: k < i < result.Length ==> result[i] in avoidSet;
+    //    assert forall i :: 0 <= i <= k ==> result[i] !in avoidSet;
 
     calc {
-      2 * |avoidSet| - k - 1;
-      <= m_workList.Length - k - 1;
-      == |multiset(result[k+1..])|;
-      <= { suffix_multiset_subset(result[..], k + 1);
-          card_multiset_subset(multiset(result[k+1..]), multiset(avoidSet)); }
-      |avoidSet|;
+       2 * |avoidSet| - k - 1;
+    <= m_workList.Length - k - 1;
+    == |multiset(result[k+1..])|;
+    <= { suffix_multiset_subset(result[..], k + 1);
+         card_multiset_subset(multiset(result[k+1..]), multiset(avoidSet)); }
+       |avoidSet|;
     }
 
-//    assert |avoidSet| <= j; // a contradiction with j + n == |avoidSet| && n > 0
+    //    assert |avoidSet| <= j; // a contradiction with j + n == |avoidSet| && n > 0
   } else {
     // assume multiset(result[..]) == multiset(m_workList[..]);
-  // assume result.Length == m_workList.Length;
-  assert uniq(m_workList[..]);
-  // assume uniq(result[..]);
-  // assume forall i :: 0 <= i < |avoidSet| ==> result[i] !in avoidSet;
+    // assume result.Length == m_workList.Length;
+    assert uniq(m_workList[..]);
+    // assume uniq(result[..]);
+    // assume forall i :: 0 <= i < |avoidSet| ==> result[i] !in avoidSet;
 
   }
 }

getRandomDataEntry.dfy

@@ -15,7 +15,7 @@ method swap<T>(a: array<T>, i: int, j: int)
   a[j] := t;
 }
 
-predicate uniq<T>(s: seq<T>)
+predicate uniq<T(==)>(s: seq<T>)
 {
   forall x :: x in s ==> multiset(s)[x] == 1
 }
@@ -26,10 +26,10 @@ lemma uniq_multiset_subset<T>(s1: seq<T>, s2: seq<T>)
   ensures multiset(s1) <= multiset(s2)
 {
   forall x | x in s1 ensures multiset(s1)[x] <= multiset(s2)[x] {
-//    calc {
-//      1;
-//      multiset(s1)[x];
-//    }
+    //    calc {
+    //      1;
+    //      multiset(s1)[x];
+    //    }
   }
 }
 
@@ -41,10 +41,10 @@ lemma card_multiset_subset<T>(m1: multiset<T>, m2: multiset<T>)
   }
   else {
     var x :| x in m1;
-//    assert x in m2;
-//    assert |m1| == |m1 - multiset{x}| + 1;
-//    assert |m2| == |m2 - multiset{x}| + 1;
-//    assert m1 - multiset{x} <= m2 - multiset{x};
+    //    assert x in m2;
+    //    assert |m1| == |m1 - multiset{x}| + 1;
+    //    assert |m2| == |m2 - multiset{x}| + 1;
+    //    assert m1 - multiset{x} <= m2 - multiset{x};
     card_multiset_subset(m1 - multiset{x}, m2 - multiset{x});
   }
 }
@@ -84,21 +84,21 @@ method getRandomDataEntry<T(==)>(m_workList: array<T>, avoidSet: seq<T>) returns
   }
 
   calc {
-       m_workList.Length;
-    == |multiset(m_workList[..])|;
-    <= { uniq_multiset_subset(m_workList[..], avoidSet);
-        card_multiset_subset(multiset(m_workList[..]), multiset(avoidSet)); }
-       |multiset(avoidSet)|;
-    == |avoidSet|; // a contradiction!
+     m_workList.Length;
+  == |multiset(m_workList[..])|;
+  <= { uniq_multiset_subset(m_workList[..], avoidSet);
+       card_multiset_subset(multiset(m_workList[..]), multiset(avoidSet)); }
+     |multiset(avoidSet)|;
+  == |avoidSet|; // a contradiction!
   }
-//  assert forall x :: x in m_workList[..] ==> x in avoidSet;
-//  assert uniq(m_workList[..]);
-//  multiset_subset(m_workList[..], avoidSet);
-//  assert multiset(m_workList[..]) <= multiset(avoidSet);
-//  card_multiset_subset(multiset(m_workList[..]), multiset(avoidSet));
-//  assert |multiset(m_workList[..])| <= |multiset(avoidSet)|;
-//  assert false;
-  
+  //  assert forall x :: x in m_workList[..] ==> x in avoidSet;
+  //  assert uniq(m_workList[..]);
+  //  multiset_subset(m_workList[..], avoidSet);
+  //  assert multiset(m_workList[..]) <= multiset(avoidSet);
+  //  card_multiset_subset(multiset(m_workList[..]), multiset(avoidSet));
+  //  assert |multiset(m_workList[..])| <= |multiset(avoidSet)|;
+  //  assert false;
+
   return m_workList[0];
 }
 
@@ -118,7 +118,7 @@ method fillWithRandomDataEntries<T(==, 0)>(m_workList: array<T>, n: int, avoidSe
 
   var k := m_workList.Length - 1;
   var r := 0;
-  
+
   while (k >= 0 && r < n)
     invariant k >= -1
     invariant r <= n
@@ -142,42 +142,42 @@ method fillWithRandomDataEntries<T(==, 0)>(m_workList: array<T>, n: int, avoidSe
       assert forall x :: x in out[0..r] ==> x in m_workList[(k + 1)..] && x !in avoidSet;
       // assert multiset(out[0..r]) <= multiset(m_workList[..]);
 
-//      assert e == m_workList[k];
+      //      assert e == m_workList[k];
       suffix_multiset_subset(m_workList[..], k);
       assert multiset(m_workList[k..]) <= multiset(m_workList[..]);
-//      assert uniq(m_workList[k..]);
+      //      assert uniq(m_workList[k..]);
 
       if e in out[0..r] {
         assert e in m_workList[(k + 1)..];
         calc {
-          multiset(m_workList[k..])[e];
+           multiset(m_workList[k..])[e];
           { assert m_workList[k..] == m_workList[k..k+1] + m_workList[k+1..]; }
-          multiset(m_workList[k..k+1] + m_workList[k+1..])[e];
-          >= 2; // a contradiction!
+           multiset(m_workList[k..k+1] + m_workList[k+1..])[e];
+        >= 2; // a contradiction!
         }
       }
-//      assert e !in out[0..r];
-      
+      //      assert e !in out[0..r];
+
       r := r + 1;
     }
-    
+
     k := k - 1;
   }
 
   if r < n {
-//    assert k == -1;
-//    assert forall x :: x in m_workList[..] ==> x in avoidSet || x in out[0..r];
-//    assert forall x :: x in m_workList[..] ==> x in avoidSet + out[0..r];
+    assert k == -1;
+    assert forall x :: x in m_workList[..] ==> x in avoidSet || x in out[0..r];
+    assert forall x :: x in m_workList[..] ==> x in avoidSet + out[0..r];
 
     uniq_multiset_subset(m_workList[..], avoidSet + out[0..r]);
     card_multiset_subset(multiset(m_workList[..]), multiset(avoidSet + out[0..r]));
 
-//    assert false;
+    //    assert false;
   }
   else {
-//    assert r == n;
+    //    assert r == n;
     assert out[0..n] == out[..];
   }
 
-//  assert r == n;
+  //  assert r == n;
 }

leetcode/0026-remove-duplicates-sorted.dfy

@@ -19,6 +19,7 @@ method RemveDuplicates(nums: array<int>) returns (length: int)
     invariant SortedStrict(nums[..j + 1])
     invariant i < nums.Length ==> forall k :: 0 <= k < i ==> nums[k] <= nums[i]
     invariant forall k :: 0 <= k < i ==> old(nums[k]) in nums[..j + 1]
+    invariant i < nums.Length ==> nums[j] <= nums[i]
   {
     if nums[i] != nums[j] {
       j := j + 1;

leetcode/0027-remove-element.dfy

@@ -1,23 +1,24 @@
 method RemoveElement(nums: array<int>, val: int) returns (newLength: int)
-    modifies nums
-    ensures 0 <= newLength <= nums.Length
-    ensures forall x :: x in nums[..newLength] ==> x != val
-    ensures multiset(nums[..newLength]) == multiset(old(nums[..]))[val := 0]
+  modifies nums
+  ensures 0 <= newLength <= nums.Length
+  ensures forall x :: x in nums[..newLength] ==> x != val
+  ensures multiset(nums[..newLength]) == multiset(old(nums[..]))[val := 0]
 {
-    var i := 0;
-    var j := 0;
-    while i < nums.Length
-        invariant j <= i
-        invariant i <= nums.Length
-        invariant old(nums[i..]) == nums[i..];
-        invariant multiset(nums[..j]) == multiset(old(nums[..i]))[val := 0]
-    {
-        if nums[i] != val {
-            nums[j] := nums[i];
-            j := j + 1;
-        }
-        i := i + 1;
+  var i := 0;
+  var j := 0;
+  while i < nums.Length
+    invariant j <= i
+    invariant i <= nums.Length
+    invariant old(nums[i..]) == nums[i..];
+    invariant multiset(nums[..j]) == multiset(old(nums[..i]))[val := 0]
+  {
+    if nums[i] != val {
+      nums[j] := nums[i];
+      j := j + 1;
+      assert nums[..j] == nums[..j-1] + [nums[i]];
     }
-    assert old(nums[..i]) == old(nums[..]);
-    return j;
+    i := i + 1;
+  }
+  assert old(nums[..i]) == old(nums[..]);
+  return j;
 }

leetcode/0121-stocks.dfy

@@ -5,7 +5,7 @@
 //   if a >= b then a else b
 // }
 
-function method Max(a: int, b: int): int {
+function Max(a: int, b: int): int {
   if a >= b then a else b
 }
 

leetcode/0155-min-stack.dfy

@@ -17,7 +17,7 @@ class MinStack {
   ghost var dataSeq: seq<int>
   ghost var minsSeq: seq<int>
 
-  predicate Valid() 
+  ghost predicate Valid() 
     reads this
   {
     ToSeq(data) == dataSeq && ToSeq(mins) == minsSeq && |dataSeq| == |minsSeq|
@@ -33,7 +33,7 @@ class MinStack {
     minsSeq := [];
   }
 
-  predicate method IsEmpty()
+  predicate IsEmpty()
     reads this
     requires Valid()
     ensures IsEmpty() <==> |dataSeq| == 0

leetcode/0167-two-sum-ii.dfy

@@ -3,7 +3,7 @@ include "../lib/Seq.dfy"
 
 import opened Seq
 
-function method TwoSumF(numbers: seq<int>, target: int, left: int, right: int) : (int, int)
+function TwoSumF(numbers: seq<int>, target: int, left: int, right: int) : (int, int)
 requires 0 <= left <= right < |numbers|;
 requires Sorted(numbers);
 decreases right - left;

leetcode/0226-invert-binary-tree.dfy

@@ -3,7 +3,7 @@ include "../lib/adt/BinaryTree.dfy"
 
 import opened BinaryTree
 
-function method Mirror<T>(t: Tree<T>) : Tree<T>
+function Mirror<T>(t: Tree<T>) : Tree<T>
 {
     match t
     case Nil => Nil

lib/MinMax.dfy

@@ -1,10 +1,10 @@
 module MinMax {
 
-  function method Min(a: int, b: int): int {
+  function Min(a: int, b: int): int {
     if a <= b then a else b
   }
 
-  function method Max(a: int, b: int): int {
+  function Max(a: int, b: int): int {
     if a >= b then a else b
   }
 
@@ -29,5 +29,5 @@ module MinMax {
     ensures a == b
   {
   }
-  
+
 }

lib/Pow.dfy

@@ -43,6 +43,12 @@ module PowModule {
   lemma PowMul(x: int, y: int, e: nat)
     ensures Pow(x * y, e) == Pow(x, e) * Pow(y, e)
   {
+    if e == 0 {
+
+    }
+    else {
+      assert Pow(x*y, e-1) == Pow(x,e-1)*Pow(y,e-1);
+    }
   }
 
   lemma PowExpAdd(x: int, a: nat, b: nat)
@@ -53,10 +59,10 @@ module PowModule {
     }
   }
 
-  function method FastPow(b: int, e: nat): int
+  function FastPow(b: int, e: nat): int
     decreases e
   {
-    if e == 0 then 1 
+    if e == 0 then 1
     else if e % 2 == 0 then FastPow(b * b, e / 2)
     else b * FastPow(b, e - 1)
   }