From dbb1949da0e610bd0cc0dfe1ecc751808e928dc4 Mon Sep 17 00:00:00 2001 From: seebees Date: Tue, 20 Aug 2024 16:39:12 -0700 Subject: [PATCH] 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 --- .github/workflows/check-examples-in-docs.yml | 2 +- .github/workflows/tests.yml | 2 +- Scripts/check-examples | 2 +- src/Collections/Sequences/LittleEndianNat.dfy | 4 +- src/Collections/Sequences/Seq.dfy | 61 -------------- src/JSON/Tests.dfy | 2 +- .../Internals/ModInternals.dfy | 80 ++++++++++++++++--- src/NonlinearArithmetic/Mul.dfy | 9 ++- src/dafny/BoundedInts.dfy | 2 +- src/dafny/Collections/Seqs.dfy | 62 -------------- src/dafny/Collections/Sets.dfy | 2 +- .../Internals/ModInternals.dfy | 8 +- 12 files changed, 88 insertions(+), 148 deletions(-) diff --git a/.github/workflows/check-examples-in-docs.yml b/.github/workflows/check-examples-in-docs.yml index dd84c975..4326620c 100644 --- 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 index e025e2a1..36e3067e 100644 --- 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 index 72249b39..0117d37e 100755 --- 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 index f642f872..c4e2d06c 100644 --- 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) - 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 index 756102fc..ab0043b9 100644 --- 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(s: set): (xs: seq) - 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(s: set) returns (xs: seq) - ensures multiset(s) == multiset(xs) - { - xs := []; - var left: set := 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(xs: seq, ys: seq, 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(s: set, R: (T, T) -> bool): (xs: seq) - 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 index 8de6581b..a2bed973 100644 --- 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 index 388b06f1..aa4fb082 100644 --- 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 index 129cf12a..66d7605c 100644 --- 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 index 2486399e..7d31e1c7 100644 --- 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 index c9c7814c..d73f61b2 100644 --- 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(s: set): (xs: seq) - 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(s: set) returns (xs: seq) - ensures multiset(s) == multiset(xs) - { - xs := []; - var left: set := 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(xs: seq, ys: seq, 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(s: set, R: (T, T) -> bool): (xs: seq) - 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 index 5c904e8f..76b1e3a5 100644 --- 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 index a4c86341..a9a8ed85 100644 --- 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); } }