`fix-846`: Need relational operator to refer to value in specific program execution

[henriman]

In certain situations, we require the ability to refer to the value of an expression in a specific program execution (of the two program executions modeled by the product program construction). (@jcp19: If I remember correctly, you called this "relational operator".)

---

Consider the following type:

type UDPAddr struct {
    IP []byte
}

pred (a *UDPAddr) Mem() {
    acc(a, 1/2) && acc(a.IP)
}

requires a.Mem()
decreases
pure func (a *UDPAddr) GetIPLen() int {
    return unfolding a.Mem() in len(a.IP)
}

requires a.Mem()
requires 0 <= i && i < a.GetIPLen()
decreases
pure func (a *UDPAddr) GetIPByte(i int) byte {
    return unfolding a.Mem() in a.IP[i]
}

Now we want to implement a hyper function IsLow specifying sensitivity properties. However, due to the restriction that we are only allowed to call other hyper functions in a hyper function, there are some properties that we can't express.

1. IP is low (property using a quantified assertion)

ghost
hyper
requires a.Mem()
decreases
pure func (a *UDPAddr) IsLow() bool {
    return low(a.GetIPLen()) && forall i int :: 0 <= i && i < a.GetIPLen() &&
        low(i) ==> low(a.GetIPByte(i))

}

The call to GetIPLen is not allowed, as it is not a hyper function. Using such a relational operator, one could replace a.GetIPLen() by something like exec1(a.GetIPLen()); together with low(a.GetIPLen()), this would then express what we intended.

2. If IP has at least one element, the first element is low (property using an implication on something other than low)

ghost
hyper
requires a.Mem()
decreases
pure func (a *UDPAddr) IsLow() bool {
    return low(a.GetIPLen()) && (a.GetIPLen() > 0 ==> low(a.GetIPByte(0)))
}

Same as above, being able to replace a.GetIPLen() by something like exec1(a.GetIPLen()) would fix this.

[henriman]

Once Gobra issue #955 is fixed, this could be worked around by unfolding Mem and accessing the fields directly.