fix: Use reveal_ constant as function argument in override axiom

Source/DafnyCore/Resolver/ModuleResolver.cs

@@ -2289,6 +2289,9 @@ void InheritedTraitMembers(TopLevelDeclWithMembers cl) {
         } else if (member.IsGhost != traitMember.IsGhost) {
           reporter.Error(MessageSource.Resolver, member.tok, "overridden {0} '{1}' in '{2}' has different ghost/compiled status than in trait '{3}'",
             traitMember.WhatKind, traitMember.Name, cl.Name, trait.Name);
+        } else if (!member.IsOpaque && traitMember.IsOpaque) {
+          reporter.Error(MessageSource.Resolver, member.tok, "overridden {0} '{1}' in '{2}' must be 'opaque' since the member is 'opaque' in trait '{3}'",
+            traitMember.WhatKind, traitMember.Name, cl.Name, trait.Name);
         } else {
           // Copy trait member's extern attribute onto class member if class does not provide one
           if (!Attributes.Contains(member.Attributes, "extern") && Attributes.Contains(traitMember.Attributes, "extern")) {

Source/DafnyCore/Verifier/BoogieGenerator.cs

@@ -1042,6 +1042,14 @@ private void CreateRevealableConstant(Function f) {
         sink.AddTopLevelDeclaration(revealTrigger);
         Bpl.Expr revealTrigger_expr = new Bpl.IdentifierExpr(f.tok, revealTrigger);
         this.functionReveals[f] = revealTrigger_expr;
+
+        // If this is an override, generate:
+        //     axiom reveal_FunctionA ==> reveal_FunctionParent;
+        if (f.OverriddenFunction is { IsOpaque: true }) {
+          var revealParent = GetRevealConstant(f.OverriddenFunction);
+          var implication = BplImp(revealTrigger_expr, revealParent);
+          AddOtherDefinition(revealTrigger, new Axiom(f.tok, implication));
+        }
       }
     }
 

Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5017a.dfy

@@ -0,0 +1,138 @@
+// RUN: %testDafnyForEachResolver --expect-exit-code=4 "%s" -- --general-traits=datatype
+
+module True {
+  trait A {
+    ghost predicate Valid()
+  }
+
+  trait B extends A {
+    ghost opaque predicate Valid() { true }
+  }
+
+  method TestByRequires(b: B)
+    requires b.Valid()
+  {
+    var a: A := b;
+    assert a.Valid();
+  }
+
+  method TestByReveal(b: B) {
+    var a: A := b;
+    assert a.Valid() by {
+      reveal b.Valid();
+    }
+  }
+}
+
+module X {
+  trait A {
+    ghost predicate Valid(w: bool)
+  }
+
+  trait B extends A {
+    ghost opaque predicate Valid(x: bool) { x }
+  }
+
+  method TestByRequires(b: B, y: bool)
+    requires b.Valid(y)
+  {
+    var a: A := b;
+    assert a.Valid(y);
+  }
+
+  method TestByReveal(b: B, y: bool) {
+    var a: A := b;
+    assert a.Valid(y) by { // error: assertion violation
+      reveal b.Valid();
+    }
+  }
+}
+
+module Parameters {
+  trait A {
+    ghost predicate P<T>(t: T)
+  }
+
+  trait B extends A {
+    ghost opaque predicate P<T>(t: T) { t == t }
+  }
+
+
+  method TestByRequires(b: B)
+    requires b.P(5)
+  {
+    var a: A := b;
+    assert a.P(5);
+  }
+
+  method TestByRequires'(b: B)
+    requires b.P(6)
+  {
+    var a: A := b;
+    assert a.P(5); // error: assertion violation
+  }
+
+  method TestByRequires''(b: B)
+    requires b.P(true)
+  {
+    var a: A := b;
+    assert a.P(5); // error: assertion violation
+  }
+
+
+  method TestByReveal(b: B) {
+    var a: A := b;
+    assert a.P(5) by {
+      reveal b.P();
+    }
+  }
+
+  method TestByReveal'(b: B) {
+    var a: A := b;
+    assert a.P(true) by {
+      reveal b.P();
+    }
+  }
+}
+
+module StayOpaque {
+  trait A {
+    opaque predicate Valid()
+  }
+
+  trait B extends A {
+    opaque predicate Valid() { true }
+  }
+
+  trait C extends A {
+    opaque predicate Valid() { true }
+  }
+
+  method TestByRequires(b: B)
+    requires b.Valid()
+  {
+    var a: A := b;
+    assert a.Valid();
+  }
+
+  method TestByReveal(b: B) {
+    var a: A := b;
+    assert a.Valid() by {
+      reveal b.Valid();
+    }
+  }
+
+  method TestIndependence0(b: B, c: C) {
+    var a: A := b;
+    assert b.Valid() by { // error: revealing for C should not affect B
+      reveal c.Valid();
+    }
+  }
+
+  method TestIndependence1(b: B, c: C) {
+    var a: A := b;
+    assert a.Valid() by { // fine: revealing for C also reveals for all A's
+      reveal c.Valid();
+    }
+  }
+}

Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5017a.dfy.expect

@@ -0,0 +1,6 @@
+git-issue-5017a.dfy(45,18): Error: assertion might not hold
+git-issue-5017a.dfy(72,14): Error: assertion might not hold
+git-issue-5017a.dfy(79,14): Error: assertion might not hold
+git-issue-5017a.dfy(127,18): Error: assertion might not hold
+
+Dafny program verifier finished with 14 verified, 4 errors

Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5017b.dfy

@@ -0,0 +1,104 @@
+// RUN: %testDafnyForEachResolver --expect-exit-code=2 "%s" -- --general-traits=datatype
+
+module Opaque {
+  trait A {
+    predicate Valid()
+  }
+
+  trait B {
+    opaque predicate Valid() { true }
+  }
+
+  trait C {
+    opaque predicate Valid()
+  }
+
+
+  trait K0 extends A {
+    predicate Valid()
+  }
+  trait K1 extends A {
+    opaque predicate Valid()
+  }
+  trait K2 extends A {
+    predicate Valid() { true }
+  }
+  trait K3 extends A {
+    opaque predicate Valid() { true }
+  }
+
+  trait L0 extends B {
+    predicate Valid() { true } // error: B.Valid already has a body
+  }
+  trait L1 extends B {
+    opaque predicate Valid() { true } // error: B.Valid already has a body
+  }
+
+  trait M0 extends C {
+    predicate Valid() // error: must be opaque (since it is in C)
+  }
+  trait M1 extends C {
+    opaque predicate Valid()
+  }
+  trait M2 extends C {
+    predicate Valid() { true } // error: must be opaque (since it is in C)
+  }
+  trait M3 extends C {
+    opaque predicate Valid() { true }
+  }
+
+
+  datatype W0 extends A = W0 {
+    predicate Valid() { true }
+  }
+  class W1 extends A {
+    predicate Valid() { true }
+  }
+
+  datatype X0 extends A = X0 {
+    opaque predicate Valid() { true }
+  }
+  class X1 extends A {
+    opaque predicate Valid() { true }
+  }
+
+  datatype Y0 extends C = Y0 {
+    predicate Valid() { true } // error: must be opaque (since it is in C)
+  }
+  class Y1 extends C {
+    predicate Valid() { true } // error: must be opaque (since it is in C)
+  }
+
+  datatype Z0 extends C = Z0 {
+    opaque predicate Valid() { true }
+  }
+  class Z1 extends C {
+    opaque predicate Valid() { true }
+  }
+}
+
+module StayOpaque {
+  trait A {
+    opaque predicate Valid()
+  }
+
+  datatype B extends A = B {
+    opaque predicate Valid() { true }
+  }
+
+  class C extends A {
+    opaque predicate Valid() { true }
+  }
+
+  method TestA(a: A) {
+    reveal a.Valid(); // error: nothing to reveal
+  }
+
+  method TestB(b: B) {
+    reveal b.Valid();
+  }
+
+  method TestC(c: C) {
+    reveal c.Valid();
+  }
+}

Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5017b.dfy.expect

@@ -0,0 +1,10 @@
+git-issue-5017b.dfy(31,14): Error: fully defined predicate 'Valid' is inherited from trait 'B' and is not allowed to be re-declared
+git-issue-5017b.dfy(34,21): Error: fully defined predicate 'Valid' is inherited from trait 'B' and is not allowed to be re-declared
+git-issue-5017b.dfy(34,21): Error: static lemma 'reveal_Valid' is inherited from trait 'B' and is not allowed to be re-declared
+git-issue-5017b.dfy(38,14): Error: overridden predicate 'Valid' in 'M0' must be 'opaque' since the member is 'opaque' in trait 'C'
+git-issue-5017b.dfy(44,14): Error: overridden predicate 'Valid' in 'M2' must be 'opaque' since the member is 'opaque' in trait 'C'
+git-issue-5017b.dfy(66,14): Error: overridden predicate 'Valid' in 'Y0' must be 'opaque' since the member is 'opaque' in trait 'C'
+git-issue-5017b.dfy(69,14): Error: overridden predicate 'Valid' in 'Y1' must be 'opaque' since the member is 'opaque' in trait 'C'
+git-issue-5017b.dfy(94,13): Error: member 'reveal_Valid' does not exist in trait 'A'
+git-issue-5017b.dfy(94,18): Error: expression has no reveal lemma
+9 resolution/type errors detected in git-issue-5017b.dfy