Rework how to handle sensitivity with interfaces

[henriman]

Current approach

In addition to Mem, I introduced a LowMem predicate containing the necessary sensitivity information.

This approach has a few problems, the most notable here being:

• LowMem needs to repeat the access permissions in Mem in order to make the sensitvity information self-framing. This leads to awkwardly splitting up the access permissions, replacing Mem() by acc(Mem(), 1/2) && acc(LowMem(), 1/2)
• In case we don't want to always require the underlying data to be low (only sometimes; in some context we might need this information, in another context it might not be necessary or not possible), working with LowMem gets rather tedious and requires a lot of changes (cf. the current approach to strings.Builder)

(Note that my approach to instead use an abstract predicate together with "unfolding/folding functions" is not sound, as the underlying data may be changed without "invalidating" LowMem.)

New suggested approach

I add a new function to the interface, indicating whether the underlying data is low or not.

ghost
requires Mem()
decreases
pure func IsLow() bool

Due to Gobra issue 846, IsLow can currently not be implemented. However, in the meantime, we can introduce abstract "reveal/hide functions" to work with IsLow anyway. Consider e.g. a struct S with one field x int:

requires s.Mem()
decreases
pure func (s *S) GetX() int {
    return unfolding s.Mem() in s.x
}

ghost
requires p > 0 && acc(s.Mem(), p) && s.IsLow()
ensures acc(s.Mem(), p) && low(s.GetX())
decreases
func (s *S) RevealIsLow(p perm)

ghost
requires p > 0 && acc(s.Mem(), p) && low(s.GetX())
ensures acc(s.Mem(), p) && s.IsLow()
decreases
func (s *S) HideIsLow(p perm)

This approach doesn't suffer from the disadvantages listed above (and is also sound; as IsLow depends on Mem, after modifying the underlying data IsLow doesn't hold anymore and we need to establish it again).

Furthermore, this is close to how we would prefer to specify sensitivity for interfaces; once Gobra issue 846 is resolved, we can just implement IsLow concretely (and either remove the reveal/hide functions, or simply introduce a body).

The only drawback I have encountered up to now can be seen in pkg/addr/isdas_spec.gobra, where both IA and *IA implement different interfaces specifying such IsLow functions; implementing IsLow for IA (s.t. (*IA).IsLow should resolve to this method as well) leads to strange error messages, which can't be worked around in the same way as 449. However, by giving the functions distinct names across the interfaces, this can be worked around as well.

---

Still contains workarounds for bugs:

• (939) Cannot write an implementation proof that would allow IA and *IA to share the same IsLow for their respective interfaces

[jcp19]

Yes, much better! I have a few minor comments that should be addressed before merging

[henriman]

I have added some improvements to this branch beyond how to handle sensitivity with interfaces. For this reason, I will close this PR (and PR #3) and open a new PR (#5) for merging sif-pkg-addr-rework into sif-private-topology. The approach described here is the one that will be used from now on, however.

[henriman]

Note that since closing this PR, I preferred calling HideIsLow AssertIsLow instead.