Simplify interface of service_read
The current specification of service_read
exposes too many details to module service_mgr
. We should reduce this specification to ease the proof.
The current specification of service_read
exposes too many details to module service_mgr
. We should reduce this specification to ease the proof.