Fix local_service_treatment
The address_space module produces an integer variable named local_service_treatment
. It is used to detect that we are processing an internal request within the server and allows bypassing the access control checks (which are for clients only).
This variable can overflow and is the cause of several failed proofs.
It should be changed to a Boolean flag, that we can set and unset. We can then use the call stack to store intermediate values and ensure that it is always properly reset after the processing of a local request.