Fix: No more mention of reveal lemmas when implementing opaque functions in traits

[MikaelMayer]

This PR fixes #2612
After investigation

1. The traits were correctly generating the reveal lemmas with a body of null
2. Reveal lemmas are compiled in a special way to Boogie, so that's why they don't need a body
3. Lemmas are methods, and a method with a null body has to be implemented in classes.

That was what caused the bug to appear. I fixed it by adding a special case to the error, so that if it's a lemma and it has the attribute specially created for lemmas that mark it opaque_reveal, then the error is not thrown.
Because of 2) this is sound.

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

[cpitclaudel]

The fix is good, but can you extend the test to check whether :opaque propagates to the classes implementing the trait? (Or if it doesn't, to confirm that it doesn't?)

[MikaelMayer]

The fix is good, but can you extend the test to check whether :opaque propagates to the classes implementing the trait? (Or if it doesn't, to confirm that it doesn't?)

I'm not sure what you mean? Can you please elaborate?

[cpitclaudel]

I'm not sure what you mean? Can you please elaborate?

Yes, sorry: I was asking about what happens when you put opaque on a signature without a body:

trait T {
  function {:opaque} F(): int
}

class C extends T {
  function F() : int { 3 }
}

method Main() {
  var c := new C;
  assert c.F() == 3;
}

[MikaelMayer]

I'm not sure what you mean? Can you please elaborate?

Yes, sorry: I was asking about what happens when you put opaque on a signature without a body:

trait T {
  function {:opaque} F(): int
}

class C extends T {
  function F() : int { 3 }
}

method Main() {
  var c := new C;
  assert c.F() == 3;
}

Good question. That will not cause any problem I can think of. Since the function in the trait is {:opaque}, there is a lemma that is generated without a body.
The code that checked that all bodiless methods have a body is not considering whether the function was marked as predicate or not.

[fabiomadge]

@cpitclaudel Your latest example passes. My first impulse was to let the user do what they deem appropriate, but the following doesn't verify, so I'm inclined to follow the precedent:

trait T {
  function F(): int
}

class C extends T {
  function F() : nat { 3 }
}

I don't think this needs to be in the scope of this PR.

[cpitclaudel]

Looks good to me! But:

trait TTT {
  function {:opaque} FFF(): int
}

class CCC extends TTT {
  function FFF() : int { 412 }
}

method M0() {
  var c := new CCC;
  assert c.FFF() == 412; // This passes
}

method M1() {
  var c := new CCC;
  reveal c.FFF();
  assert c.FFF() == 412; // This fails
}

The difference between M0 and M1 is the type inference:

method M0'() {
  var c: TTT := new CCC;
  assert c.FFF() == 412; // This fails
}

method M1'() {
  var c: CCC := new CCC;
  reveal c.FFF();
  assert c.FFF() == 412; // This passes
}

Should I open a separate issue for this?

[MikaelMayer]

Looks good to me! But:

trait TTT {
  function {:opaque} FFF(): int
}

class CCC extends TTT {
  function FFF() : int { 412 }
}

method M0() {
  var c := new CCC;
  assert c.FFF() == 412; // This passes
}

method M1() {
  var c := new CCC;
  reveal c.FFF();
  assert c.FFF() == 412; // This fails
}

The difference between M0 and M1 is the type inference:

method M0'() {
  var c: TTT := new CCC;
  assert c.FFF() == 412; // This fails
}

method M1'() {
  var c: CCC := new CCC;
  reveal c.FFF();
  assert c.FFF() == 412; // This passes
}

Should I open a separate issue for this?

Yes, I think the issue here is that {:opaque} attribute are not ported from the traits to the classes, or something else.