chore: Improve tests #5859

RustanLeino · 2024-10-25T22:50:36Z

Overview

This PR improves several test cases in the Dafny test suite to make them relies less on old/deprecated features and to make them more stable. My intent here is to still preserve the goal of each test.

These changes came about from trying to run Dafny with a new version of Z3, but the PR itself does not change the version of Z3 being used.

Details

dafny0/SeqFromArray.dfy
Changed quantified properties into checks for a single arbitrary value.
dafny0/TypeConversions.dfy
Changed one method's use of bv67 to bv7. This is because Z3 has a tough time converting between integers and. large bitvectors. As one data point of the current state of such conversions, I also added to the test file the times required for other bitvector tests.
dafny2/SmallestMissingNumber-functional.dfy
Use opaque, turning off induction, add some inline lemmas (assert), and remove the no longer needed isolate_assertions.
dafny4/Lucas-down.legacy.dfy
Remove the unnecessary use of the legacy flag /arith. Rename the test file to Lucas-down.dfy.
dafny4/Lucas-up.legacy.dfy
Remove the need for /arith, use opaque, turn off automatic induction, and write proofs by hand.
dafny4/Primes.dfy
Use opaque.
git-issues/git-issue-2301.dfy
Disentangle tests by using several methods/functions, and avoid hitting the max-5 error limit (which previously had masked one error).
git-issues/git-issue-3855.dfy
Replace \d with [0-9] to support the test on platforms where sed doesn't understand \d.
lambdas/MatrixAssoc.dfy
Explicitly indicate which variable to do the induction on.
triggers/emptyTrigger.dfy
Change == to <= to avoid making the test do different things if (a new version of) Z3 optimizes quantifiers like exists z :: ... && z == E into ... with z replaced by E.
wishlist/sequences-s0-in-s.dfy
Disentangle tests into separate methods.

By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.

typerSniper · 2024-11-13T16:45:54Z

Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/TypeConversions.dfy

-
-method M4() returns (x: int, n: nat, r: real, even: EvenInt, small: SmallReal, b67: bv67, w: bv32, seven: bv7, noll: bv0)
-  ensures UseTheVars(x, n, r, even, small, b67, w, seven, noll)
+// M4 is checked quickly, but using bv67 instead of bv7 takes forever, and even bv23 takes 40 minutes. See numbers at bottom of this file.


could remove one of seven or bv7 from the inputs.

typerSniper · 2024-11-13T18:16:41Z

Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny2/SmallestMissingNumber-functional.dfy

@@ -90,7 +90,7 @@ function SMN''(xs: List<nat>, n: nat, len: nat): nat
      SMN''(R, n + llen, len - llen)
 }

-function Split(xs: List<nat>, b: nat): (List<nat>, List<nat>)
+opaque function Split(xs: List<nat>, b: nat): (List<nat>, List<nat>)


I like this opaque.

However, I don't understand why we need Split_Correct as a separate lemma. I tried adding the requires and ensures clauses of Split_Correct directly into the function and it verifies. So, something to consider.

And, its a subjective thing, but when the stated property is the definition of a function and can be proved directly, I think its cleaner to have it in the function.

I often make the decision based on if the property is one I think all users of the function are going want. If it is, then I add it as a postcondition of the function. Otherwise, I make it into a separate lemma.

In this case, the property stated by Split_Correct is relevant only in situations where the input has no duplicates. Since the Split function doesn't require the no-duplicates property, I think the lemma is best stated separately.

Why are you using opaque here, instead of hide on the consumer side?

I think opaque should only be placed on functions whose behavior is fully defined by their ensures clauses. Here's a PR that applies that principle to all of the standard library: #5781

typerSniper · 2024-11-13T18:17:59Z

Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny2/SmallestMissingNumber-functional.dfy

@@ -194,10 +194,20 @@ lemma Split_Correct(xs: List<nat>, b: nat)
    Elements(r.1) == (set x | x in Elements(xs) && b <= x) &&
    NoDuplicates(r.0) && NoDuplicates(r.1)
 {
+  var split := Split(xs, b);


We wouldn't need this lemma if we incoroprate the comment above.

typerSniper · 2024-11-13T18:30:42Z

Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny2/SmallestMissingNumber-functional.dfy

@@ -206,17 +216,38 @@ lemma Elements_Property(xs: List)
 {
 }

-ghost function IntRange(lo: nat, len: nat): set<nat>
-  ensures |IntRange(lo, len)| == len
+opaque ghost function IntRange(lo: nat, len: nat): (s: set<nat>)


Consider the following function definition and removing FormSet entirely.

opaque ghost function IntRange(lo: nat, len: nat): (s: set<nat>) decreases len ensures |s| == len ensures forall x :: x in s <==> lo <= x < lo + len { if (len == 0) then {} else IntRange (lo + 1, len - 1) + {lo} }

Good suggestions.

typerSniper · 2024-11-13T18:43:16Z

Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny2/SmallestMissingNumber-functional.dfy

@@ -236,22 +267,30 @@ lemma {:isolate_assertions} SMN'_Correct(xs: List<nat>, n: nat, len: nat)
    var bound := IntRange(n, half);
    Cardinality(Elements(L), bound);
    if llen < half {
+      reveal SMN'();


SMN' is not opaque

typerSniper · 2024-11-13T18:45:19Z

Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny2/SmallestMissingNumber-functional.dfy

      SMN'_Correct(L, n, llen);
    } else {
-      var s := SMN'(R, n + llen, len - llen);
+      var s := SMN'(xs, n, len);
+      var t := SMN'(R, n + llen, len - llen);


perhaps don't need to define t here. Two options: (i) remove the definition and replace t by s in the assert by below, (ii) move the definition of t into the assert by.

I moved it into the assert by.

# Conflicts: # Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/Lucas-up.dfy

keyboardDrummer · 2024-11-14T13:45:05Z

Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/Lucas-up.dfy

@@ -48,14 +49,20 @@ lemma BitSize(i: nat, n: nat)

 // An easy-to-read name for the expression that checks if a number
 // is even.
-ghost predicate EVEN(n: nat)
+opaque ghost predicate EVEN(n: nat)


Again, try to avoid introducing opaque function in our tests

Because opaque functions are more cumbersome to use then regular ones. They need to be revealed any time you want the body to be visible, and are hidden in contexts even where no reduction in resource count is needed.

You can see the code size advantage of avoiding opaque functions in the refactoring in this PR: #5781

RustanLeino added 3 commits October 25, 2024 15:44

Improve tests

92c1b83

Remove need for .legacy

043ec8e

Merge branch 'master' into improve-tests

e53a7af

RustanLeino marked this pull request as ready for review October 30, 2024 21:18

RustanLeino enabled auto-merge (squash) October 30, 2024 21:18

RustanLeino added 4 commits October 31, 2024 18:12

Merge branch 'master' into improve-tests

a9e90e8

Merge branch 'master' into improve-tests

9e07e12

Merge branch 'master' into improve-tests

dc4c035

Merge branch 'master' into improve-tests

6484dc7

typerSniper reviewed Nov 13, 2024

View reviewed changes

RustanLeino added 3 commits November 13, 2024 13:49

Remove parameter “b7” in favor of parameter “seven”

e7fc1b6

Improve code/proofs in test

97411f8

Merge branch 'master' into improve-tests

64dd990

# Conflicts: # Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/Lucas-up.dfy

keyboardDrummer reviewed Nov 14, 2024

View reviewed changes

typerSniper previously approved these changes Nov 15, 2024

View reviewed changes

RustanLeino added 2 commits November 15, 2024 09:28

Merge branch 'master' into improve-tests

b026c43

Try adding back in isolate_assertions to pass CI on github

7937120

RustanLeino dismissed typerSniper’s stale review via 7937120 November 15, 2024 18:07

typerSniper approved these changes Nov 17, 2024

View reviewed changes

RustanLeino merged commit b998ed9 into dafny-lang:master Nov 17, 2024
22 checks passed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

chore: Improve tests #5859

chore: Improve tests #5859

RustanLeino commented Oct 25, 2024

typerSniper Nov 13, 2024

typerSniper Nov 13, 2024

typerSniper Nov 13, 2024

RustanLeino Nov 13, 2024

keyboardDrummer Nov 14, 2024

typerSniper Nov 13, 2024

typerSniper Nov 13, 2024

RustanLeino Nov 13, 2024

typerSniper Nov 13, 2024

typerSniper Nov 13, 2024

RustanLeino Nov 13, 2024

keyboardDrummer Nov 14, 2024

RustanLeino Nov 14, 2024

keyboardDrummer Nov 15, 2024 •

edited

Loading

chore: Improve tests #5859

chore: Improve tests #5859

Conversation

RustanLeino commented Oct 25, 2024

Overview

Details

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

keyboardDrummer Nov 15, 2024 • edited Loading

Choose a reason for hiding this comment

keyboardDrummer Nov 15, 2024 •

edited

Loading