fix: Don't generate the "assume T.F(ins) == C.F(ins)" statement in the function override ensures check

[robin-aws]

Fixes #2500.

As described in #2500, this assume statement (assume B.Class.TotallyNotZero(this) == A.Trait.TotallyNotZero(this); in the example) may create a contradiction if the implementation violates the trait's function specification. It is also not necessary to form the proof obligation correctly, since the trait's declaration has to have no body and therefore assuming equivalence doesn't add any additional constraint anyway.

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

[robin-aws]

This seems to imply that an implementing function can have more parameters than the trait-declared version. Given that this broke zero tests, it either a) doesn't exist as a feature (anymore?), or b) has no testing coverage. My gut tells me this was implemented optimistically but never used. If no one knows the history here I can dig into it.

[robin-aws]

The diff here is deceptive: removing the builder.Add(TrAssumeCmd(...)) line makes half of the lines here unused, but the other half is still needed if there is a result variable declared. Consider this as a two step edit: first removing those interspersed unneeded lines, and then moving the remainder inside the if (resultVariable != null) block.

[cpitclaudel]

Wrong section of the release notes.

[cpitclaudel]

Could you give a version of this example that doesn't use {:termination false}?

[cpitclaudel]

Unfortunately, this fix isn't sufficient, as the fixed Dafny still accepts the following example:

module A {
  trait {:termination false} Trait {
    function method TotallyNotZero() : (ret: int)
      ensures TotallyNotZero() != 0
  }
}

module Main {
  import opened A

  class Class extends Trait {
    function method TotallyNotZero() : (ret: int) {
      0
    }
  }

  method Boom() ensures false {
    var c := new Class;
    assert c.TotallyNotZero() == 0;
    assert (c as Trait).TotallyNotZero() != 0;
  }
}

(Notice the fact that ensures now mentions TotallyNotZero)

The problem really is linked to :termination false, and specifically the fact that the postcondition of the trait function "leaks" into the override check.

[cpitclaudel]

After reading it, I also expected your patch to break the following case:

trait Trait {
  function method TotallyNotZero() : (ret: int)
    ensures TotallyNotZero() != 0
}

class Class extends Trait {
  function method TotallyNotZero() : (ret: int) {
    0
  }
}

Since we would get the following:

implementation {:verboseName "Class.TotallyNotZero (override check)"} OverrideCheck$$_module.Class.TotallyNotZero(this: ref) returns (ret#0: int)
{
  var Class_$_Frame: <beta>[ref,Field beta]bool;

    assert true;
    Class_$_Frame := (lambda<alpha> $o: ref, $f: Field alpha :: 
      $o != null && read($Heap, $o, alloc) ==> false);
    assert (forall<alpha> $o: ref, $f: Field alpha :: false ==> false);
    // assert _module.Class.TotallyNotZero(this) == _module.Trait.TotallyNotZero(this);
    assume _module.Class.TotallyNotZero(this) == ret#0;
    assert _module.Trait.TotallyNotZero(this) != 0;
}

… and how would Boogie prove _module.Trait.TotallyNotZero() != 0 without knowing that _module.Class.TotallyNotZero(this) == _module.Trait.TotallyNotZero(this)? But in fact it knows that regardless of whether we comment the // line above or not:

// override axiom for _module.Trait.TotallyNotZero in class _module.Class
axiom 1 <= $FunctionContextHeight
   ==> (forall this: ref :: 
    { _module.Trait.TotallyNotZero(this), $Is(this, Tclass._module.Class()) } 
      { _module.Trait.TotallyNotZero(this), _module.Class.TotallyNotZero(this) } 
    this != null && $Is(this, Tclass._module.Class())
       ==> _module.Trait.TotallyNotZero(this) == _module.Class.TotallyNotZero(this));

(And indeed uncommenting this axiom while keeping your patch makes the valid example above fail.)

[cpitclaudel]

The reason I mention the override axiom is that it is "as powerful", modulo fuel issues, as the assume that this PR is removing, and in fact causes the same issue (I'm not sure it can be triggered from Dafny directly, though). Morally the issue is here:

module A {
  trait {:termination false} Trait {
    function method TotallyNotZero() : (ret: int)
      ensures ret != 0
  }
}

import opened A

class Class extends Trait {
  function method TotallyNotZero() : (ret: int)
    ensures (this as Trait).TotallyNotZero() != 0
  { 0 }
}

method Boom() ensures false {
  var c := new Class;
  assert c.TotallyNotZero() == 0;
  assert (c as Trait).TotallyNotZero() != 0;
}

The mere mention of (this as Trait).TotallyNotZero() is enough to trigger the axiom and hence restore the problem, even with the assume removed (but note that that mention also exploits :termination false, so it's cheating; adding the mention directly at the boogie level works, though).

[fabiomadge]

I think this PR solves the actual issue at hand. That is incorrectly performing the overrides check in a multi module setting, while correctly doing so in a single module. All the counterexamples I've seen, also rely on the lack of termination checking, which is documented.
We should add additional protection to the overrides axiom. To achieve this, I propose repurposing the $FunctionContextHeight mechanism.