assert Gcd(2,2)==2 fails

[hmijail]

Dafny version

4.0.0

Code to produce this issue

In the Power User note KRML279[1], a Gcd function is defined. The code is also present at Test/dafny4/gcd.dfy.

If in Main() one adds

Test(2,2); 
assert Gcd(2,2)==2;

the assertion fails, even though the result of running the code is correct.

[1] https://leino.science/papers/krml279.html

Command to run and resulting output

$ dafny run Test/dafny4/gcd_modified.dfy

Dafny program verifier finished with 19 verified, 0 errors
2 gcd 2  =  2

What happened?

I expected the assert to pass.

What type of operating system are you experiencing the problem on?

Mac

[MikaelMayer]

I converted the issue to a discussion because if Dafny can't prove something, it does not mean the thing isn't true or that Dafny is bogus, it only means Dafny needs more guidance. It's not because the Fermat theorem is true that Dafny should be able to prove assert forall x, y, z, n | n > 2 ::Power(x, n) + Power(y, n) == Power(z, n) ==> x == y == z == 0. Try to prove that GCD(2, 2) == 2 by hand. Given the mathematics definitions, it's not obvious.

Here is what you can enter to help Dafny prove what you want:

assert Gcd(2,2)==2 by {
    assert Factors(2) == {1, 2} by {
      calc {
        Factors(2);
        set p: pos | p <= 2 && IsFactor(p, 2);
        { 
          assert IsFactor(1, 2) by {
            assert 1 * 2 == 2;
          }
          assert IsFactor(2, 2) by {
            assert 2 * 1 == 2;
          }
        }
        ({1, 2});
      }
    }
    assert {1, 2} * {1, 2} == {1, 2};
    assert Max({1, 2}) == 2;
  }

Once you establish such a proof, you can try to omit some terms because Dafny can automate some of it. Here is the minimal proof I've found:

  assert Gcd(2,2)==2 by {
    assert 1 * 2 == 2 * 1; // Just there to trigger IsFactor
    assert Factors(2) == {1, 2};
    assert Factors(2) * Factors(2) == {1, 2};
  }

[MikaelMayer]

I googled "Dafny triggers"
Could you please open an issue in Dafny to precisely describe how the documentation was misleading? I'd appreciate.

Good spot for the markdown issue. I just fixed it. Thanks.

[hmijail]

I've been thinking how to express my problem with the documentation regarding this issue. Please let me know if this is helpful and if so I will create a new issue:

My feeling is that until relatively recently the ubiquitous advice I heard about working with Dafny was to break down any logical steps into smaller and smaller steps until asserts would pass. I got this from both Dafny docs and from more experienced colleagues. This is still the message in existing pages (like "Lemmas and Induction", or the already mentioned GCD page - in these the word "trigger" never appears).

Notably, those same more experienced colleagues were surprised when lately I mentioned that there seems to be growing attention to hiding information for verification durability instead of just providing more and more asserts.

It is in this context that I felt unable to understand how to strike any balance to help Dafny prove that gcd(2,2)==2:

• on one hand assert 1*2 == 2*1 felt hopelessly trivial; if I have to add that, surely I will also need to add lots of other mysteriously trivial asserts.
• on the other hand, I'm supposed to be careful with adding asserts to not misguide the solver.
• and to top it off, I didn't even know if my problem was that I had too much or too little information for the solver. In summary I was lost and I didn't even know where was the goal anyway.

But now the concept that it's not the assert 1*2 == 2*1 that is useful, but the syntactic pattern, allows me to escape that dilemma and gives me a different understanding of what was missing; there's a different way to poke the black box.

I think that before this issue I only heard about triggers from some diagnostic message in Dafny. I somehow survived that case and forgot about the whole thing, and I had no idea they were somehow involved here - since there was no warning or anything mentioning them. Maybe it is that Dafny has managed to automate triggers away so well that when that automation failed it left me without a clue of what was wrong?
So I understand now that triggers are generally important, and I will be paying more attention to them and to their annotations.

Feature Request: add an option to make automatic annotations (decrease, tail recursive, triggers) much more visible (inline like counterexamples, instead of the current small squiggle). I imagine this would be a great learning aid.

[hmijail]

I just realized that the FAQ about triggers says

Arithmetic is not allowed in triggers

... and goes on to give x + y as a disallowed example.

But meanwhile the Verification Optimization page's explicit triggers example uses x * z and y * z.

Also: I just tried looking for some treatment of triggers on the Program Proofs book, and couldn't find anything.

So I am thinking that more documentation about triggers would be helpful.

[MikaelMayer]

Weird indeed @RustanLeino I would love an explanation on that.

[atomb]

Yes, we should definitely update the documentation to clarify the situation.

It's unfortunately for a fairly technical reason that I would hope that we wouldn't need to expose to Dafny users, but at the moment is necessary in some situations. The underlying SMT solver allows triggers to be defined for any user-defined function, but not for the built-in operations it has special understanding of. Arithmetic operations are generally among those built-in operations. The /noNLarith and /arith flags introduce new wrappers around the built-in operations which then allow them to be used in triggers but make Z3 less able to reason about them directly. The effect is that you're able to write more quantified lemmas about them, but also that you need to write more lemmas about them.