Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

"the method must provide an equal or more permissive precondition than in its parent trait" when marking a predicate opaque #2941

Closed
cpitclaudel opened this issue Oct 28, 2022 · 0 comments · Fixed by #4033
Labels
incompleteness Things that Dafny should be able to prove, but can't kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label

Comments

@cpitclaudel
Copy link
Member

cpitclaudel commented Oct 28, 2022

The code:

trait T {
  predicate Valid(x: int)
  method MyMethod(x: int) requires Valid(x)
}

class C extends T {
  predicate {:opaque} Valid(x: int) { true }
  method MyMethod(x: int) requires Valid(x) {
  }
}

Incorrectly shows the error:

the method must provide an equal or more permissive precondition than in its parent trait

Boogie code:

    assume _module.T.Valid(this, x#0);
    assert _module.C.Valid(StartFuelAssert__module.C.Valid, this, x#0);

With `{:opaque} the following axioms are missing:

// layer synonym axiom
axiom (forall $ly: LayerType, this: ref, x#0: int ::
  { _module.C.Valid($LS($ly), this, x#0) }
  _module.C.Valid($LS($ly), this, x#0) == _module.C.Valid($ly, this, x#0));

// fuel synonym axiom
axiom (forall $ly: LayerType, this: ref, x#0: int ::
  { _module.C.Valid(AsFuelBottom($ly), this, x#0) }
  _module.C.Valid($ly, this, x#0) == _module.C.Valid($LZ, this, x#0));

… but they are not enough (since we don't know the value of StartFuelAssert__module.C.Valid

Reported by @MikaelMayer .

@cpitclaudel cpitclaudel added kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label incompleteness Things that Dafny should be able to prove, but can't labels Oct 28, 2022
MikaelMayer added a commit that referenced this issue May 17, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
incompleteness Things that Dafny should be able to prove, but can't kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label
Projects
None yet
Development

Successfully merging a pull request may close this issue.

1 participant