feat: Method calls with a by-proof

[fabiomadge]

Fixes #5582. To enable this, we split method calls into two separate calls on the boogie level.

TODAY:
  // check termination...
  call z := Call$$MyMethod(u);

AFTER SPLITTING Call$$, we have:
  // check termination...
  call Call_Pre$$MyMethod(u);
  call z := Call_Post$$MyMethod(u);

FOR CALL-BY, WE HAVE:
   // check termination...
   if (*) {
     // include the proof here
     LemmaAboutP();
     call Call_Pre$$MyMethod(u);
     assume false;
   }
   call z := Call_Post$$MyMethod(u);

[keyboardDrummer]

Can you use hide instead of opaque, because I think we'll be switching to hide entirely.

[fabiomadge]

How would I go about that? I didn't find it in the reference manual.

[keyboardDrummer]

It's not released yet, but it's in the master ref manual. You have to add hide P or hide * somewhere in your method. At the top works.

[fabiomadge]

It seems more verbose to me. I correctly understand, that I would need to add it to every method, right?

[keyboardDrummer]

It seems more verbose to me. I correctly understand, that I would need to add it to every method, right?

Correct. If you want to cut the verbosity per test, you can add another predicate with no body and a lemma that proves it with no body, that will be similar to an opaque one.

For the test where you reveal something though, you need either an opaque thing or a hide statement, but I think we should not add any more usage of opaque to our test-suite, since I think the feature will be marked as deprecated soon.

[fabiomadge]

I think both hide and opaque achieve the same thing, but in different ways. I don't see why we shouldn't let our users choose which they prefer.

This feature targets both the old and the new resolver, so I want to test it with both. I'd need to add another test file that only targets the new resolver to test hide, which doesn't feel worth it to me. The proliferation of tests files makes finding things harder.

[keyboardDrummer]

I think both hide and opaque achieve the same thing, but in different ways. I don't see why we shouldn't let our users choose which they prefer.

If one is strictly better than the other, than giving the choice will be confusing for the user. However, better to discuss this on the deprecation PR.

The proliferation of tests files makes finding things harder.

Does the amount of files relate to that? Everything in one file would be the first IMO. I think we should structure the test files according to how the AST is structured, but that's something for the future.

I think having testing coverage will always be more important than minimizing the amount of test files. Revealing a hidden function might be the most common statement that occurs in a method call by clause, so let's add a test for that.

[fabiomadge]

From what I gather, hide is just another frontend to the existing, and tested, reveal mechanism, but if you want that test, you can have it.

[keyboardDrummer]

From what I gather, hide is just another frontend to the existing, and tested, reveal mechanism

What makes you think that? It's not.

but if you want that test, you can have it.

Thanks

[fabiomadge]

In that case, fair enough. I should have looked harder.