Is there a way to verify the equivalence of two dafny annotations?

[ChuyueSun]

Summary

Say I want to verify the equivalence of two dafny annotations. Currently my method is to first verify the programs' precondition equivalence and then postcondition' equivalence in the following format:

predicate pre_original(a: array<int>,key: int,index: int)
reads a
{
true
}

predicate pre_gen(a: array<int>,key: int,index: int)
reads a
{
true
}

lemma pre_eq(a: array<int>,key: int,index: int)
        ensures pre_original(a,key,index ) <==> pre_gen(a,key,index )
 {
}

predicate post_original(a: array<int>,key: int,index: int)
requires pre_original(a,key,index)
reads a
{
( -1<=index<a.Length) && ( index!=-1 ==> a[index]==key) && ( index == -1 ==> (forall i::0 <= i < a.Length ==> a[i] != key))
}

predicate post_gen(a: array<int>,key: int,index: int)
requires pre_gen(a,key,index)
reads a
{
 (0 <= index < a.Length &&  a[index] == key) ||
((index == -1) && (forall k :: 0 <= k < a.Length ==> a[k] != key))
}

lemma post_eq(a: array<int>,key: int,index: int)
        requires pre_original(a,key,index )
        requires pre_gen(a,key,index )
        ensures post_original(a,key,index ) <==> post_gen(a,key,index )
 {
}

Background and Motivation

If I were to do it this way, then predicates disallow me to use old expression, so I cannot verify any postconditions like

predicate post_original(a: array<int>)
requires pre_original(a)
reads a
{
( old(a[4]) +3 == a[4]) && ( a[8] == old(a[8])) && ( a[7]==516)
}

predicate post_gen(a: array<int>)
requires pre_gen(a)
reads a
{
( a[8] == old(a[8])) && ( a[7] == 516) && ( a[4] == old(a[4]) + 3)
}

lemma post_eq(a: array<int>) 
        requires pre_original(a ) 
        requires pre_gen(a ) 
        ensures post_original(a ) <==> post_gen(a ) 
 {
}

Is there a better way to do it?

Proposed Feature

Verify annotation equivalence

Alternatives

No response

[MikaelMayer]

"old" is assuming that there are two heaps in scope, the old one and the current one. To ensure you have access to this construct, please replace predicate with twostate predicate.