{:termination false} also allows incorrect implementations of trait functions

[robin-aws]

Classes are not allowed to extend a trait in another module unless {:termination false} is present on the trait. The details of the unsoundness this avoids are in this issue: #1588

The implication of this attribute is only that a failure to terminate might not be caught by the verifier, but there also seem to be other cases not strictly related to termination proof conditions:

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

module B {

  import opened A

  class Class extends Trait {
    constructor() {}
    function TotallyNotZero() : (ret: int)
      // Missing: ensures ret != 0
    { 
      0 
    }
  }

  method Main() {
    var asClass: Class := new Class();
    var asTrait: Trait := asClass;
    assert asClass.TotallyNotZero() == asTrait.TotallyNotZero();
    assert false;
  }
}

Moving the Trait trait inside module B causes the missing post-condition onClass.TotallyNotZero to be flagged correctly.

This may be by design because of the limitations of modular verification, but at the very least {:termination false} needs to be documented much better regardless. The name also does not imply opting in to this kind of unsoundness.

[robin-aws]

This seems to be a result of the verification condition generated for the override check assuming that the functions defined on the trait and the class are equivalent (the <-- highlighted line below).

implementation {:verboseName "B.Class.TotallyNotZero (override check)"} OverrideCheck$$B.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);
    assume B.Class.TotallyNotZero(this) == A.Trait.TotallyNotZero(this); <-- 
    assume B.Class.TotallyNotZero(this) == ret#0;
    assert ret#0 != 0;
} 

When B.Class.TotallyNotZero’s post-conditions do not imply A.Trait.TotallyNotZero’s, and its implementation in fact definitely violates them, that assumption introduces a contradiction, and therefore we can’t trust a successful verification of the final assert. I confirmed that changing the body of B.Class.TotallyNotZero to any non-zero value causes the expected verification failure on the override check.

[robin-aws]

Note the "workaround" to this is to always copy the specifications on trait elements onto the implementing elements in any implementing class.

[cpitclaudel]

Some more notes on this issue:

The assume B.Class.TotallyNotZero(this) == A.Trait.TotallyNotZero(this); is not the problem, per se, because (1) there is a separate axiom that states the same thing:

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

If we remove the assume the trigger for it also goes away, but depending on triggers for correctness is icky.

… and because (2) the spec of the predicate can also be written as TotallyNotZero() != 0 instead of ret != 0, in which case the axiom will trigger anyway.

The source of the problem seems to be related to termination metrics. Specifically, because of {:termination false}, Dafny exports the following axiom in B:

axiom true
   ==> (forall this: ref :: 
    { A.Trait.TotallyNotZero(this) } 
    A.Trait.TotallyNotZero#canCall(this)
         || (this != null && $Is(this, Tclass.A.Trait()))
       ==> A.Trait.TotallyNotZero(this) != 0);

The version in A, on the other hand, has an additional hypothesis on the function call height:

axiom 0 <= $FunctionContextHeight
   ==> (forall this: ref :: 
    { A.Trait.TotallyNotZero(this) } 
    A.Trait.TotallyNotZero#canCall(this)
         || (0 != $FunctionContextHeight && this != null && $Is(this, Tclass.A.Trait()))
       ==> A.Trait.TotallyNotZero(this) != 0);

The result is that the following verifies:

procedure OverrideCheck$$B.Class.TotallyNotZero();

implementation OverrideCheck$$B.Class.TotallyNotZero()
{
  var this: ref;
  assume this != null && $Is(this, Tclass.B.Class()) ;
  assert A.Trait.TotallyNotZero(this) != 0;
}

[cpitclaudel]

Reclassifying this away from soundness, since it depends on :termination false, which is opt-in and documented to be unsound.

The fixes here are either

1. Address Termination of dynamic dispatch #1588 in full
2. Drop modularity when verifying code that uses :termination false (verify everything together in one giant call graph)

[cpitclaudel]

I'm classifying this back to soundness, following a conversation with @robin-aws . The problem here is not so much that :termination false allows unsoundness through nontermination (which is fine, it's documented to do that), it's that :termination false breaks your code even if you don't have nontermination.

This is not the intent of this feature, at least based on what the docs say:

Caution: This loophole is unsound; that is, if a cross-module dynamic
dispatch fails to terminate, then this and other errors in the program
may have been overlooked by the verifier.

(emphasis mine)

So we should fix the docs or fix the feature, but the current situation seems akin to saying "assume is unsound" and then deriving false from assume true (iow: yes, assume can let you write incorrect things, and so can :termination false, but it shouldn't lead Dafny to prove false when you didn't actually write incorrect things)

[cpitclaudel]

Today @fabiomadge and I discussed about this issue. The following example shows why "just" locking the consequence axiom of the trait function under a context height constraint is not enough:

module A {
  trait {:termination false} TTT {
    function FFF(): int
      ensures FFF() > 7
  }

  function method ReExpose(ttt: TTT): int
    ensures ttt.FFF() > 7
  { 0 }
}

module B {
  import opened A

  class CCC extends TTT {
    function FFF(): int
      ensures ReExpose(this) == 0
    { 0 }
  }
}

This example verifies even if the consequence axiom is removed from the Boogie module that we generate for B.

[cpitclaudel]

One thing that we didn't explore in depth is whether it would be possible to rewrite the override check to remove all mentions of the trait and the class function, and instead just prove forall r, class.post(r) ==> trait.post(r). The difficulty there is what to do with calls to other functions on the same trait.

[fabiomadge]

This example verifies even if the consequence axiom is removed from the Boogie module that we generate for B.

It isn't valid when checking termination, though.

[robin-aws]

PR was reverted for completeness issues