# Library prosa.analysis.facts.SBF

Require Export prosa.analysis.definitions.sbf.pred.
Require Export prosa.analysis.facts.behavior.supply.
Require Export prosa.model.task.concept.
In this section, we prove some useful facts about SBF.
Section SupplyBoundFunctionLemmas.
Consider any type of tasks ...
Context {Task : TaskType}.
... and any type of jobs.
Context {Job : JobType}.
Context `{JobArrival Job}.
Context `{JobCost Job}.
Consider any kind of unit-supply processor state model, ...
Context `{PState : ProcessorState Job}.
Hypothesis H_unit_supply_proc_model : unit_supply_proc_model PState.
... any valid arrival sequence, ...
Variable arr_seq : arrival_sequence Job.
Hypothesis H_valid_arrivals : valid_arrival_sequence arr_seq.
... and any schedule.
Variable sched : schedule PState.
In the following section, we prove a lemma about switching a predicate inside of valid_pred_sbf.
Section SBFChangePred.
Consider an SBF ...
Context {SBF : SupplyBoundFunction}.
... and two predicates P1 and P2 such that, for any job j and a time interval `[t1, t2)`, P2 j t1 t2 implies P1 j t1 t2.
Variables P1 P2 : Job → instant → instant → Prop.
Hypothesis H_p2_implies_p1 :
∀ j t1 t2,
arrives_in arr_seq j →
P2 j t1 t2 → P1 j t1 t2.
Then if SBF is a valid SBF w.r.t. predicate P1, then SBF is a valid SBF w.r.t. predicate P2.
Lemma valid_pred_sbf_switch_predicate :
valid_pred_sbf arr_seq sched P1 SBF →
valid_pred_sbf arr_seq sched P2 SBF.
Proof.
move⇒ VAL; split; first by apply VAL.
move⇒ j t1 t2 ARR P2j t NEQ.
by eapply VAL ⇒ //.
Qed.
End SBFChangePred.
Consider an arbitrary predicate on jobs and time intervals.
Variable P : Job → instant → instant → Prop.
Consider a supply-bound function SBF that is valid w.r.t. the predicate P. That is, (1) SBF 0 = 0 and (2) for any job j, an interval `[t1, t2)` satisfying P j, and a subinterval `[t1, t) ⊆ [t1, t2)`, the supply produced during the time interval `[t1, t)` is at least SBF (t - t1).
Context {SBF : SupplyBoundFunction}.
Hypothesis H_valid_SBF : valid_pred_sbf arr_seq sched P SBF.
In this section, we show a simple upper bound on the blackout during an interval of length Δ.
Section BlackoutBound.
Consider any job j.
Variable j : Job.
Hypothesis H_arrives_in : arrives_in arr_seq j.
Consider an interval `[t1, t2)` satisfying P j.
Variables t1 t2 : instant.
Hypothesis H_P_interval : P j t1 t2.
Consider an arbitrary duration Δ such that t1 + Δ ≤ t2.
Variable Δ : duration.
Hypothesis H_subinterval : t1 + Δ ≤ t2.
We show that the total blackout time during an interval of length Δ is bounded by Δ - SBF Δ.
Lemma blackout_during_bound_SBF :
blackout_during sched t1 (t1 + Δ) ≤ Δ - SBF Δ.
Proof.
rewrite blackout_during_complement // leq_sub ⇒ //.
rewrite -(leqRW (snd H_valid_SBF _ _ _ _ _ _ _)).
{ by have → : (t1 + Δ) - t1 = Δ by lia. }
{ by apply H_arrives_in. }
{ by eapply H_P_interval. }
{ lia. }
Qed.
End BlackoutBound.
In the following section, we prove a few facts about unit SBF.
Section UnitSupplyBoundFunctionLemmas.
In addition, let us assume that SBF is a unit-supply SBF. That is, SBF makes steps of at most one.
Hypothesis H_unit_SBF : unit_supply_bound_function SBF.
We prove that the complement of such an SBF (i.e., fun Δ ⇒ Δ - SBF Δ) is monotone.
Lemma complement_SBF_monotone :
∀ Δ1 Δ2,
Δ1 ≤ Δ2 →
Δ1 - SBF Δ1 ≤ Δ2 - SBF Δ2.
Proof.
move ⇒ Δ1 Δ2 LE; interval_to_duration Δ1 Δ2 k.
elim: k ⇒ [|δ IHδ]; first by rewrite addn0.
by rewrite (leqRW IHδ) addnS (leqRW (H_unit_SBF _)); lia.
Qed.
End UnitSupplyBoundFunctionLemmas.
End SupplyBoundFunctionLemmas.