service_on instead of service_in in the class ProcessorState

This merge request is related to @mlesourd’s MR !101 (closed): it aims at only providing one aspect of !101 (closed), to help merging the later in the future.

The aspect we consider here can be seen in the changes of behavior/schedule.v: all the other changes are consequences of it. The class ProcessorState contains a type Core, and a function scheduled_on : Job -> State -> Core -> bool stating whether a given job is scheduled on a particular core. From this, the definition scheduled_in : Job -> State -> bool states that there exists a core such that this job is scheduled in it. Note that this definition doesn’t assume that a job is only scheduled on one core at a time (I don’t know whether this is plausible or not). This part doesn’t change in this MR.

The class ProcessorState also defines functions about the service. This is the part changing in this MR.

Before, a function service_in : Job -> State -> work was defined, returning the total amount of service a job get among all cores. With this MR, a function service_on : Job -> State -> Core -> work is defined instead, and service_in is later defined as the sum of service on all cores. This way of defining service_in from service_on is similar to the way scheduled_in` and scheduled_on` are defined.

This MR is thus changing the definition of service_in. This should not cause great issues as service_in is declared opaque, however several files in the development makes it locally transparent: changing the definition of service_in breaks all these parts. In particular, in the case of the ideal processor, there is only one core, and service_in is equal to the value of service_on on this particular core… however the general definition of service_in as a sum is not convertible to this. To this end, I’m adding lemmas in analysis/facts/model/ideal_schedule.v: service_in_def rewrites service_in in the case of the ideal processor as the definition that proofs in which service_in was made locally transparent expect. This remove the need to make service_in transparent in most cases.

Another possibility (idea from @sophie) to still have a service_on, but without changing the definition of service_in, would be to add an hypothesis that a job can’t receive service in more than one core at the same time, and retrieve service_on using scheduled_on and service_in:

Definition service_on j s c := if scheduled_on j s c then service_in j s else 0.

This would have the advantage of not having to update these proofs, but would come as a cost: service_on/service_in would not follow the same scheme than scheduled_on/scheduled_in, and we would have to carry an additional hypothesis (service can’t be given on more than one core for a given job—which is probably a reasonable hypothesis, but would require more work when defining an instance of ProcessorState).

I’m still experimenting with Prosa, so I’m super happy to receive any feedback ☺