Improved DataPlaneMutexInvariant contracts

[LinoTelschow]

From the Run method and all the way down in the call graph we need the following condition to hold:
unfolding acc(DataPlaneMutexInvariant(d), _) in d.Metrics != nil && d.svc != nil && d.internal != nil

As Is:

• currently we assume this in the Run method and propagate this information down the call graph.

To Be:

• Use an approach, that can establish these conditions in the setter methods, before Run gets called.

João's idea:

• we introduce, at least, three abstract predicates: d.InitializedMetrics(), d.InitializedServices(), and d.InitializedInternal().
• These permissions are generated only on the corresponding setter methods, when they do not produce an error.
• We introduce ghost methods for each of this fields to allow us to obtain the knowledge that the fields are non nil when they are initialized. Check [1] for an example for the metrics field.
• We add the access to a wildcard permission of d.InitializedMetrics(), d.InitializedServices(), and d.InitializedInternal() to this method.

This approach is still based on some assumptions, specifically that after initialization, the value of these fields is not changed - otherwise, some function that has write permission to these fields could change them to nil. We can fix this too by changing the permissions of these fields in the DataPlane Invariant to 1/2, and require the other half to be provided to the setter methods (but not returned), thus guaranteeing that after a call to a setter method, the fields cannot be rewritten.

[1]:

ghost
requires acc(DataPlaneMutexInvariant(d)) // could be changed to acc(DataPlaneMutexInvariant(d), _)
requires acc(d.InitializedMetrics(), _)
ensures unfolding acc(DataPlaneMutexInvariant(d), _) in d.Metrics != nil
func (d *DataPlane) initializedMetricsAreNonNil()