Changes to avoid unnecessary assumptions

[jcp19]

After a conversation with @mlimbeck, we figured that the specs that we use in the router are sometimes a bit awkward and force us to introduce a few adhoc assumptions (e.g., assume d.WellConfigured() in Run) which can be made into preconditions if we change slightly our predicates. The goal of this PR is to restructure the predicates used in the dataplane to avoid such assumptions, and to eliminate the need for calling // @ IgnoreFromHere() before the call to d.mtx.Unlock in Run. In the process, we changed slightly the specifications of some public methods in a few ways:

• they no longer access private fields in the specification, except for d.mtx. We can easily address this later, and it is not urgent at all
• they are a bit more permissive in terms of preconditions (and may allow to return nil)
• due to an incompleteness in the closure encoding, we were not able to call the read closure from inside other closures. To overcome that, we manually asserted the preconditions (there are no postconditions to establish). This is cumbersome, ugly, and prone to errors when specs change. In this PR, I introduce a much better temporary fix that requires passing d as a parameter to the closure, which allows us to perform the call.
  To avoid unnecessary work at the moment, we did not update the postconditions to preserve information hiding in the setters as well. Instead, we dropped them for now and we plan to add them lazily, on a per-need basis.

This PR can be seen as a step towards addressing #155 (although completely solving that would require strengthening Gobra's type system).

While doing this PR, I also noticed a few unused ghost methods and some small issues that I fixed.

I also run into a very annoying incompleteness in the termination checker of Viper that I will likely report reported (viperproject/silver#773 (comment)) as a bug.

Finally, verifying Run now seems to be much faster due to better info hiding. However, verifying initMetrics takes much longer. I could spend some time looking into this, but given our current priorities and the fact that the spec of this method should not change again, it is better to spend my time somewhere else.

The only thing missing to conclude this PR is to refactor Run. Once that is done, this PR is ready for review and for merging