Remove warnings in forall (#158)

* Remove warnings * Remove SetToSeq The method makes it difficult to use the libraries in a project that enables `--enforce-determinism`. * Don't show snippets when checking examples * Fix some non-linear proofs --------- Co-authored-by: Aaron Tomb <aarotomb@amazon.com>
dafny-lang · Aug 20, 2024 · dbb1949 · dbb1949
1 parent e9b898d
commit dbb1949
Show file tree

Hide file tree

Showing 12 changed files with 88 additions and 148 deletions.
diff --git a/.github/workflows/check-examples-in-docs.yml b/.github/workflows/check-examples-in-docs.yml
@@ -14,7 +14,7 @@ jobs:
     strategy:
       fail-fast: false
       matrix:
-        version: [ 3.13.1, 4.0.0 ]
+        version: [ 4.0.0 ]
         os: [ ubuntu-latest ]
 
     runs-on: ${{ matrix.os }}

diff --git a/.github/workflows/tests.yml b/.github/workflows/tests.yml
@@ -13,7 +13,7 @@ jobs:
   verification:
     strategy:
       matrix:
-        version: [ 3.13.1, 4.0.0, 4.1.0, 4.2.0 ]
+        version: [ 4.0.0, 4.1.0 ]
 
     uses: ./.github/workflows/reusable-tests.yml
     with:

diff --git a/Scripts/check-examples b/Scripts/check-examples
@@ -76,7 +76,7 @@ defaultCommand=
 defaultExit=
 defaultLang=
 useHeadings=0
-defOptions="--function-syntax:4 --use-basename-for-filename --unicode-char:false"
+defOptions="--function-syntax:4 --use-basename-for-filename --unicode-char:false --show-snippets=false"
 legacyOptions="-functionSyntax:4 -useBaseNameForFileName"
 
 while getopts 'md:x:l:' opt; do

diff --git a/src/Collections/Sequences/LittleEndianNat.dfy b/src/Collections/Sequences/LittleEndianNat.dfy
@@ -308,8 +308,8 @@ abstract module {:options "-functionSyntax:4"} LittleEndianNat {
   /* The nat representation of a sequence and its least significant position are
   congruent. */
   lemma LemmaSeqLswModEquivalence(xs: seq<uint>)
-    requires |xs| >= 1;
-    ensures IsModEquivalent(ToNatRight(xs), First(xs), BASE());
+    requires |xs| >= 1
+    ensures IsModEquivalent(ToNatRight(xs), First(xs), BASE())
   {
     if |xs| == 1 {
       LemmaSeqLen1(xs);

diff --git a/src/Collections/Sequences/Seq.dfy b/src/Collections/Sequences/Seq.dfy
@@ -846,65 +846,4 @@ module {:options "-functionSyntax:4"} Seq {
       result := next + result;
     }
   }
-
-  /**********************************************************
-   *
-   *  Sets to Ordered Sequences
-   *
-   ***********************************************************/
-
-  /* Converts a set to a sequence (ghost). */
-  ghost function SetToSeqSpec<T>(s: set<T>): (xs: seq<T>)
-    ensures multiset(s) == multiset(xs)
-  {
-    if s == {} then [] else var x :| x in s; [x] + SetToSeqSpec(s - {x})
-  }
-
-  /* Converts a set to a sequence (compiled). */
-  method SetToSeq<T>(s: set<T>) returns (xs: seq<T>)
-    ensures multiset(s) == multiset(xs)
-  {
-    xs := [];
-    var left: set<T> := s;
-    while left != {}
-      invariant multiset(left) + multiset(xs) == multiset(s)
-    {
-      var x :| x in left;
-      left := left - {x};
-      xs := xs + [x];
-    }
-  }
-
-  /* Proves that any two sequences that are sorted by a total order and that have the same elements are equal. */
-  lemma SortedUnique<T(!new)>(xs: seq<T>, ys: seq<T>, R: (T, T) -> bool)
-    requires SortedBy(xs, R)
-    requires SortedBy(ys, R)
-    requires TotalOrdering(R)
-    requires multiset(xs) == multiset(ys)
-    ensures xs == ys
-  {
-    assert |xs| == |multiset(xs)| == |multiset(ys)| == |ys|;
-    if xs == [] || ys == [] {
-    } else {
-      assert xs == [xs[0]] + xs[1..];
-      assert ys == [ys[0]] + ys[1..];
-      assert multiset(xs[1..]) == multiset(xs) - multiset{xs[0]};
-      assert multiset(ys[1..]) == multiset(ys) - multiset{ys[0]};
-      assert multiset(xs[1..]) == multiset(ys[1..]);
-      SortedUnique(xs[1..], ys[1..], R);
-    }
-  }
-
-  /* Converts a set to a sequence that is ordered w.r.t. a given total order. */
-  function SetToSortedSeq<T(!new)>(s: set<T>, R: (T, T) -> bool): (xs: seq<T>)
-    requires TotalOrdering(R)
-    ensures multiset(s) == multiset(xs)
-    ensures SortedBy(xs, R)
-  {
-    MergeSortBy(SetToSeqSpec(s), R)
-  } by method {
-    xs := SetToSeq(s);
-    xs := MergeSortBy(xs, R);
-    SortedUnique(xs, SetToSortedSeq(s, R), R);
-  }
 }
diff --git a/src/JSON/Tests.dfy b/src/JSON/Tests.dfy
@@ -134,7 +134,7 @@ module JSON.Tests {
     // Stress test - this used to cause stack overflow errors because of non-tail-recursive functions.
     // We should have these kinds of tests direclty in the Unicode module too.
     "\"" + Seq.Repeat('a', 100_000) + "\""
-  ];
+  ]
 
   method Main() {
     ZeroCopyWrapper.TestStrings(VECTORS);

diff --git a/src/NonlinearArithmetic/Internals/ModInternals.dfy b/src/NonlinearArithmetic/Internals/ModInternals.dfy
@@ -84,16 +84,31 @@ module {:options "-functionSyntax:4"} ModInternals {
     }
   }
 
+
+
   lemma LemmaDivAddDenominator(n: int, x: int)
     requires n > 0
     ensures (x + n) / n == x / n + 1
   {
     LemmaFundamentalDivMod(x, n);
     LemmaFundamentalDivMod(x + n, n);
+    assert x + n == n * ((x + n) / n) + ((x + n) % n);
     var zp := (x + n) / n - x / n - 1;
-    forall ensures 0 == n * zp + ((x + n) % n) - (x % n) { LemmaMulAuto(); }
-    if (zp > 0) { LemmaMulInequality(1, zp, n); }
-    if (zp < 0) { LemmaMulInequality(zp, -1, n); }
+    assert 0 == n * zp + ((x + n) % n) - (x % n) by { LemmaMulDistributes(); }
+    if (zp > 0) {
+      assert (x + n) / n == x / n + 1 by {
+        LemmaMulInequality(1, zp, n);
+        assert n <= zp * n;
+        assert n <= x;
+      }
+    }
+    if (zp < 0) {
+      assert (x + n) / n == x / n + 1 by {
+        LemmaMulInequality(zp, -1, n);
+        assert zp * n <= -n;
+        assert n <= x;
+      }
+    }
   }
 
   lemma LemmaDivSubDenominator(n: int, x: int)
@@ -102,22 +117,49 @@ module {:options "-functionSyntax:4"} ModInternals {
   {
     LemmaFundamentalDivMod(x, n);
     LemmaFundamentalDivMod(x - n, n);
+    assert x - n == n * ((x - n) / n) + ((x - n) % n);
     var zm := (x - n) / n - x / n + 1;
-    forall ensures 0 == n * zm + ((x - n) % n) - (x % n) { LemmaMulAuto(); }
-    if (zm > 0) { LemmaMulInequality(1, zm, n); }
-    if (zm < 0) { LemmaMulInequality(zm, -1, n); }
+    assert 0 == n * zm + ((x - n) % n) - (x % n) by { LemmaMulDistributes(); }
+    if (zm > 0) {
+      assert (x - n) / n == x / n - 1 by {
+        LemmaMulInequality(1, zm, n);
+        assert n <= zm * n;
+        assert n <= x;
+      }
+    }
+    if (zm < 0) {
+      assert (x - n) / n == x / n - 1 by {
+        LemmaMulInequality(zm, -1, n);
+        assert n <= zm * -n;
+        assert n <= x;
+      }
+    }
   }
 
+
   lemma LemmaModAddDenominator(n: int, x: int)
     requires n > 0
     ensures (x + n) % n == x % n
   {
     LemmaFundamentalDivMod(x, n);
     LemmaFundamentalDivMod(x + n, n);
+    assert x + n == n * ((x + n) / n) + ((x + n) % n);
     var zp := (x + n) / n - x / n - 1;
-    forall ensures 0 == n * zp + ((x + n) % n) - (x % n) { LemmaMulAuto(); }
-    if (zp > 0) { LemmaMulInequality(1, zp, n); }
-    if (zp < 0) { LemmaMulInequality(zp, -1, n); }
+    assert 0 == n * zp + ((x + n) % n) - (x % n) by { LemmaMulDistributes(); }
+    if (zp > 0) {
+      assert (x + n) % n == x % n by {
+        LemmaMulInequality(1, zp, n);
+        assert n <= zp * n;
+        assert n <= x;
+      }
+    }
+    if (zp < 0) {
+      assert (x + n) % n == x % n by {
+        LemmaMulInequality(zp, -1, n);
+        assert zp * n <= -n;
+        assert n <= x;
+      }
+    }
   }
 
   lemma LemmaModSubDenominator(n: int, x: int)
@@ -126,12 +168,26 @@ module {:options "-functionSyntax:4"} ModInternals {
   {
     LemmaFundamentalDivMod(x, n);
     LemmaFundamentalDivMod(x - n, n);
+    assert x - n == n * ((x - n) / n) + ((x - n) % n);
     var zm := (x - n) / n - x / n + 1;
-    forall ensures 0 == n * zm + ((x - n) % n) - (x % n) { LemmaMulAuto(); }
-    if (zm > 0) { LemmaMulInequality(1, zm, n); }
-    if (zm < 0) { LemmaMulInequality(zm, -1, n); }
+    assert 0 == n * zm + ((x - n) % n) - (x % n) by { LemmaMulDistributes(); }
+    if (zm > 0) {
+      assert (x - n) % n == x % n by {
+        LemmaMulInequality(1, zm, n);
+        assert n <= zm * n;
+        assert n <= x;
+      }
+    }
+    if (zm < 0) {
+      assert (x - n) % n == x % n by {
+        LemmaMulInequality(zm, -1, n);
+        assert n <= zm * -n;
+        assert n <= x;
+      }
+    }
   }
 
+
   lemma LemmaModBelowDenominator(n: int, x: int)
     requires n > 0
     ensures 0 <= x < n <==> x % n == x

diff --git a/src/NonlinearArithmetic/Mul.dfy b/src/NonlinearArithmetic/Mul.dfy
@@ -243,7 +243,14 @@ module {:options "-functionSyntax:4"} Mul {
     ensures forall x: int, XBound: int, y: int, YBound: int {:trigger x * y, (XBound - 1) * (YBound - 1)}
               :: x < XBound && y < YBound && 0 < x && 0 < y ==> x * y <= (XBound - 1) * (YBound - 1)
   {
-    forall (x: int, XBound: int, y: int, YBound: int | x < XBound && y < YBound && 0 < x && 0 < y)
+    forall (x: int, XBound: int, y: int, YBound: int
+      // https://github.com/dafny-lang/dafny/issues/4771
+      {:trigger (XBound - 1) * (YBound - 1), x * y}
+      {:trigger YBound - 1, XBound - 1, 0 < y, 0 < x}
+      {:trigger YBound - 1, 0 < y, x < XBound}
+      {:trigger XBound - 1, 0 < x, y < YBound}
+      {:trigger y < YBound, x < XBound}
+      | x < XBound && y < YBound && 0 < x && 0 < y)
       ensures x * y <= (XBound - 1) * (YBound - 1)
     {
       LemmaMulStrictUpperBound(x, XBound, y, YBound);

diff --git a/src/dafny/BoundedInts.dfy b/src/dafny/BoundedInts.dfy
@@ -25,7 +25,7 @@ module {:options "-functionSyntax:4"} Dafny.BoundedInts {
   const TWO_TO_THE_128: int := 0x1_00000000_00000000_00000000_00000000
   const TWO_TO_THE_256: int := 0x1_00000000_00000000_00000000_00000000_00000000_00000000_00000000_00000000
   const TWO_TO_THE_512: int :=
-    0x1_00000000_00000000_00000000_00000000_00000000_00000000_00000000_00000000_00000000_00000000_00000000_00000000_00000000_00000000_00000000_00000000;
+    0x1_00000000_00000000_00000000_00000000_00000000_00000000_00000000_00000000_00000000_00000000_00000000_00000000_00000000_00000000_00000000_00000000
 
   newtype uint8 = x: int   | 0 <= x < TWO_TO_THE_8
   newtype uint16 = x: int  | 0 <= x < TWO_TO_THE_16

diff --git a/src/dafny/Collections/Seqs.dfy b/src/dafny/Collections/Seqs.dfy
@@ -803,68 +803,6 @@ module {:options "-functionSyntax:4"} Dafny.Collections.Seq {
   }
 
 
-  /**********************************************************
-   *
-   *  Sets to Ordered Sequences
-   *
-   ***********************************************************/
-
-  /* Converts a set to a sequence (ghost). */
-  ghost function SetToSeqSpec<T>(s: set<T>): (xs: seq<T>)
-    ensures multiset(s) == multiset(xs)
-  {
-    if s == {} then [] else var x :| x in s; [x] + SetToSeqSpec(s - {x})
-  }
-
-  /* Converts a set to a sequence (compiled). */
-  method SetToSeq<T>(s: set<T>) returns (xs: seq<T>)
-    ensures multiset(s) == multiset(xs)
-  {
-    xs := [];
-    var left: set<T> := s;
-    while left != {}
-      invariant multiset(left) + multiset(xs) == multiset(s)
-    {
-      var x :| x in left;
-      left := left - {x};
-      xs := xs + [x];
-    }
-  }
-
-  /* Proves that any two sequences that are sorted by a total order and that have the same elements are equal. */
-  lemma SortedUnique<T(!new)>(xs: seq<T>, ys: seq<T>, R: (T, T) -> bool)
-    requires SortedBy(xs, R)
-    requires SortedBy(ys, R)
-    requires TotalOrdering(R)
-    requires multiset(xs) == multiset(ys)
-    ensures xs == ys
-  {
-    assert |xs| == |multiset(xs)| == |multiset(ys)| == |ys|;
-    if xs == [] || ys == [] {
-    } else {
-      assert xs == [xs[0]] + xs[1..];
-      assert ys == [ys[0]] + ys[1..];
-      assert multiset(xs[1..]) == multiset(xs) - multiset{xs[0]};
-      assert multiset(ys[1..]) == multiset(ys) - multiset{ys[0]};
-      assert multiset(xs[1..]) == multiset(ys[1..]);
-      SortedUnique(xs[1..], ys[1..], R);
-    }
-  }
-
-  /* Converts a set to a sequence that is ordered w.r.t. a given total order. */
-  function SetToSortedSeq<T(!new)>(s: set<T>, R: (T, T) -> bool): (xs: seq<T>)
-    requires TotalOrdering(R)
-    ensures multiset(s) == multiset(xs)
-    ensures SortedBy(xs, R)
-  {
-    MergeSortBy(SetToSeqSpec(s), R)
-  } by method {
-    xs := SetToSeq(s);
-    xs := MergeSortBy(xs, R);
-    SortedUnique(xs, SetToSortedSeq(s, R), R);
-  }
-
-
   /****************************
    **  Sorting sequences
    ***************************** */

diff --git a/src/dafny/Collections/Sets.dfy b/src/dafny/Collections/Sets.dfy
@@ -229,7 +229,7 @@ module {:options "-functionSyntax:4"} Dafny.Collections.Sets {
   {
     var range := SetRange(a, b);
     forall e {:trigger e in range}{:trigger e in x} | e in x
-      ensures e in range;
+      ensures e in range
     {
     }
     assert x <= range;

diff --git a/src/dafny/NonlinearArithmetic/Internals/ModInternals.dfy b/src/dafny/NonlinearArithmetic/Internals/ModInternals.dfy
@@ -91,7 +91,7 @@ module {:options "-functionSyntax:4"} Dafny.ModInternals {
     LemmaFundamentalDivMod(x, n);
     LemmaFundamentalDivMod(x + n, n);
     var zp := (x + n) / n - x / n - 1;
-    forall ensures 0 == n * zp + ((x + n) % n) - (x % n) { LemmaMulAuto(); }
+    assert 0 == n * zp + ((x + n) % n) - (x % n) by { LemmaMulAuto(); }
     if (zp > 0) { LemmaMulInequality(1, zp, n); }
     if (zp < 0) { LemmaMulInequality(zp, -1, n); }
   }
@@ -103,7 +103,7 @@ module {:options "-functionSyntax:4"} Dafny.ModInternals {
     LemmaFundamentalDivMod(x, n);
     LemmaFundamentalDivMod(x - n, n);
     var zm := (x - n) / n - x / n + 1;
-    forall ensures 0 == n * zm + ((x - n) % n) - (x % n) { LemmaMulAuto(); }
+    assert 0 == n * zm + ((x - n) % n) - (x % n) by { LemmaMulAuto(); }
     if (zm > 0) { LemmaMulInequality(1, zm, n); }
     if (zm < 0) { LemmaMulInequality(zm, -1, n); }
   }
@@ -115,7 +115,7 @@ module {:options "-functionSyntax:4"} Dafny.ModInternals {
     LemmaFundamentalDivMod(x, n);
     LemmaFundamentalDivMod(x + n, n);
     var zp := (x + n) / n - x / n - 1;
-    forall ensures 0 == n * zp + ((x + n) % n) - (x % n) { LemmaMulAuto(); }
+    assert 0 == n * zp + ((x + n) % n) - (x % n) by { LemmaMulAuto(); }
     if (zp > 0) { LemmaMulInequality(1, zp, n); }
     if (zp < 0) { LemmaMulInequality(zp, -1, n); }
   }
@@ -127,7 +127,7 @@ module {:options "-functionSyntax:4"} Dafny.ModInternals {
     LemmaFundamentalDivMod(x, n);
     LemmaFundamentalDivMod(x - n, n);
     var zm := (x - n) / n - x / n + 1;
-    forall ensures 0 == n * zm + ((x - n) % n) - (x % n) { LemmaMulAuto(); }
+    assert 0 == n * zm + ((x - n) % n) - (x % n) by { LemmaMulAuto(); }
     if (zm > 0) { LemmaMulInequality(1, zm, n); }
     if (zm < 0) { LemmaMulInequality(zm, -1, n); }
   }