# Library prosa.analysis.facts.behavior.supply

Require Export prosa.util.all.
Require Export prosa.model.processor.platform_properties.

# Supply

In this file, we establish properties of the notion of supply.
We start with a few basic facts about supply.
Section BasicFacts.
Consider any type of jobs, ...
Context {Job : JobType}.
... any kind of processor state model, ...
Context `{PState : ProcessorState Job}.
... and any schedule.
Variable sched : schedule PState.
First, we leverage the property service_on_le_supply_on to show that service_at j t is always bounded by supply_at t.
Lemma service_at_le_supply_at :
∀ j t,
service_at sched j t ≤ supply_at sched t.
As a corollary, it is easy to show that if a job receives service at a time instant t, then the supply at this time instant is positive.
Corollary pos_service_impl_pos_supply :
∀ j t,
0 < service_at sched j t →
0 < supply_at sched t.
Next, we show that, at any time instant t, either there is some supply available or it is a blackout time.
Lemma blackout_or_supply :
∀ t,
is_blackout sched t ∨ has_supply sched t.
End BasicFacts.
As a common special case, we establish facts about schedules in which supply is either 0 or 1 at all times.
Section UnitService.
Consider any type of jobs, ...
Context {Job : JobType}.
... any kind of unit-supply processor state model, ...
Context `{PState : ProcessorState Job}.
Hypothesis H_unit_supply_proc_model : unit_supply_proc_model PState.
... and any schedule.
Variable sched : schedule PState.
We show that, under the unit-supply assumption, supply_at t is equal to 1 - is_blackout t for any time instant t.
Lemma supply_at_complement :
∀ t,
supply_at sched t = 1 - is_blackout sched t.
Vice versa, is_blackout t is equal to 1 - supply_at t, up to the bool–nat conversion.
Lemma is_blackout_complement :
∀ t,
nat_of_bool (is_blackout sched t) = 1 - supply_at sched t.
We note that supply is bounded at all times by 1 ...
Remark supply_at_le_1 :
∀ t,
supply_at sched t ≤ 1.
... and as a trivial consequence, we show that the service of any job is either 0 or 1.
Corollary unit_supply_proc_service_case :
∀ j t,
service_at sched j t = 0 ∨ service_at sched j t = 1.
We show that supply during an interval `[t, t + δ)` is bounded by δ.
Lemma supply_during_bound :
∀ t δ,
supply_during sched t (t + δ) ≤ δ.
We show that blackout during an interval `[t, t + δ)` is bounded by δ.
Lemma blackout_during_bound :
∀ t δ,
blackout_during sched t (t + δ) ≤ δ.
We observe that the supply during an interval can be decomposed into the last instant and the rest of the interval.
Lemma supply_during_last_plus_before :
∀ t1 t2,
t1 ≤ t2 →
supply_during sched t1 t2.+1 = supply_during sched t1 t2 + supply_at sched t2.
We show a similar lemma for blackout_during.
Lemma blackout_during_last_plus_before :
∀ t1 t2,
t1 ≤ t2 →
blackout_during sched t1 t2.+1 = blackout_during sched t1 t2 + is_blackout sched t2.
We show that the service during a time interval `[t, t + δ)` is equal to the difference between δ and the blackout during `[t, t + δ)`.
Lemma supply_during_complement :
∀ t δ,
supply_during sched t (t + δ) = δ - blackout_during sched t (t + δ).
Similarly, we show that the blackout during a time interval `[t, t + δ)` is equal to the difference between δ and the supply during `[t, t + δ)`.
Lemma blackout_during_complement :
∀ t δ,
blackout_during sched t (t + δ) = δ - supply_during sched t (t + δ).
The number of blackout time instants in `[t1, t2)` is equal to the sum of blackout time instants in `[t1, t)` and `[t, t2)`.
Lemma blackout_during_cat :
∀ (t1 t2 t : instant),
t1 ≤ t ≤ t2 →
blackout_during sched t1 t + blackout_during sched t t2 = blackout_during sched t1 t2.
The number of blackout time instants can increase by at most 1 when extending the interval by one unit.
Lemma blackout_during_unit_growth :
∀ (t : instant),
unit_growth_function (blackout_during sched t).
End UnitService.
Lastly, we prove one lemma about supply in the case of the fully supply-consuming processor model.
Section ConsumedSupply.
Consider any type of jobs, ...
Context {Job : JobType}.
... any kind of fully supply-consuming processor state model, ...
Context `{PState : ProcessorState Job}.
Hypothesis H_supply_is_fully_consumed : fully_consuming_proc_model PState.
... and any schedule.
Variable sched : schedule PState.
The fact that a job j is scheduled at a time instant t and there is a supply at t implies that the job receives service at time t.
Lemma progress_inside_supplies :
∀ (j : Job) (t : instant),
has_supply sched t →
scheduled_at sched j t →
0 < service_at sched j t.
End ConsumedSupply.
We add some of the above lemmas to the "Hint Database" basic_rt_facts, so the auto tactic will be able to use them.
Global Hint Resolve
supply_at_le_1
: basic_rt_facts.