How to prove static invariant (of an enum) in different heap?

[FliegendeWurst]

I have an enum JMERuleErrorType and would like to prove that its static invariant holds after some unrelated heap modifications.

So I end up with a sequent like:

fr.up.xlim.sic.ig.jerboa.jme.verif.JMERuleErrorType::<$inv>(heap),
...
==>
fr.up.xlim.sic.ig.jerboa.jme.verif.JMERuleErrorType::<$inv>(heapAfter_verifDimensionGraphArcs),
...

But I can't make use of the formula on the right. There is also no option to use a dependency contract.

[FliegendeWurst]

Here is a full example:
JMERuleErrorType.java

enum JMERuleErrorType {
  INFO,
  WARNING,
  CRITICAL;
}

Usecase.java

class Usecase {
    /*@ public normal_behavior
      @ requires \static_invariant_for(JMERuleErrorType);
      @ ensures \result != null;
      @*/
    public JMERuleErrorType produceEnum() {
        return JMERuleErrorType.INFO;
    }

    /*@ public normal_behavior
      @ requires \static_invariant_for(JMERuleErrorType);
      @ ensures \result != null;
      @*/
    public JMERuleErrorType callMethodTwice() {
        produceEnum();
        return produceEnum();
    }
}

[WolframPfeifer]

In this concrete case, you could add a postcondition ensures \static_invariant_for(JMERuleErrorType) to produceEnum. However, this is not a general solution. I think, most of the time, it should be possible to add \static_invariant_for(JMERuleErrorType) to the non-static invariant (of the class UseCase in this example). Since in the enum everything is final, I think this could be sufficient. For static invariants in general, I am not sure if this is enough. Unfortunately, as far as I know it is not possible to define dependency contracts for static invariants. I was thinking about something like accessible \static_inv: <locset_term>, however, it is not supported.