Opaque insufficiently revealing - Verification issue

[kjx]

Failing code

trait Animal {
    function           not_opaque() : ( rv : int)
    function {:opaque} iam_opaque() : ( rv : int) 

    predicate depends_on_not_opaque() 
       ensures  not_opaque() == 42 
    predicate depends_on_iam_opaque() 
       ensures  iam_opaque() == 42 
}

class Cat extends Animal {
    function           not_opaque() : ( rv : int) { 42 } 
    function {:opaque} iam_opaque() : ( rv : int) 
         //ensures rv == 42
         { reveal iam_opaque();  42 } 

    predicate depends_on_not_opaque() 
       ensures not_opaque() == 42 {true}
    predicate depends_on_iam_opaque() 
       ensures reveal iam_opaque(); iam_opaque() == 42 {reveal iam_opaque(); true}
}

Steps to reproduce the issue

• Dafny version: 4.0.0.50303
• Dafny VSCode extension version: 3.1.0

Expected behavior

I've made two sets of two parallel functions across a trait and a class
depends_on_not_opaque()'s postcondition depends on the return value of the not_opaque() function

depends_on_iam_opaque()'s postcondition is exactly the same,
except that it depends on the return value iam_opaque() function, which is opaque.
I put in "reveal iam_opaque()" everywhere I could think of at the time...

I expected both opaque and nonopaque versions would behave the same

Actual behavior

the not_opaque version works; the iam_opaque version doesn't, complaining that

the function must provide an equal or more detailed postcondition than in its parent trait

even though the postconditions is textually identical..

adding in a postcondition on the opaque version (uncommentiung the commented line //ensures rv == 42)
means everything works. I sort-of understand why, but I think I should be able to do this with reveals...

Here's what may be a related issue:

class Rat {
    function           not_opaque() : ( rv : int) { 42 } 
    function {:opaque} iam_opaque() : ( rv : int) 
         { 42 } 

    predicate depends_on_not_opaque() 
       ensures  not_opaque() == 42 {true}
    predicate depends_on_iam_opaque() 
    //   requires reveal iam_opaque(); true
      ensures reveal iam_opaque(); iam_opaque() == 42 { true}   //reveal iam_opaque(); true
}

in an attempt to get to a single-class version I tried the above.
This has a different problem: it does not verify if iam_opaque(); is revealed in the postcondition; (or in a separate ensures clause);
Error is

A postcondition might not hold on this return path.

It does verify if iam_opaque(); is revealed as a separate precondition requires reveal iam_opaque(); true
or in the body { reveal iam_opaque(); true }.

[MikaelMayer]

Seems related to #2941

[MikaelMayer]

Looking at the Boogie code, I'm see the following

    assume _module.Cat.iam__opaque(StartFuel__module.Cat.iam_opaque, this) == LitInt(42); // The reveal statement
    assert _module.Cat.iam__opaque(StartFuelAssert__module.Cat.iam_opaque, this) == LitInt(42); // The override check

The second assert should prove but it's missing the following two lines

    assume AsFuelBottom(StartFuel__module.Cat.iam_opaque)
       == StartFuel__module.Cat.iam_opaque;
    assume AsFuelBottom(StartFuelAssert__module.Cat.iam_opaque)
       == StartFuelAssert__module.Cat.iam_opaque;

which is normally added by "// initialize fuel constant". Let me fix that.