# Library prosa.implementation.facts.maximal_arrival_sequence

Require Export prosa.analysis.facts.model.task_arrivals.
Require Export prosa.implementation.definitions.maximal_arrival_sequence.
Recall that, given an arrival curve max_arrivals and a job-generating function generate_jobs_at, the function concrete_arrival_sequence generates an arrival sequence. In this section, we prove a few properties of this function.
Section MaximalArrivalSequence.
Consider any type of tasks ...
Context {Task : TaskType}.
Context `{TaskCost Task}.
... and any type of jobs associated with these tasks.
Context {Job : JobType}.
Context `{JobTask Job Task}.
Context `{JobArrival Job}.
Context `{JobCost Job}.
Consider a task set ts with non-duplicate tasks.
Variable ts : seq Task.
Hypothesis H_ts_uniq : uniq ts.
Let max_arrivals be a family of valid arrival curves, i.e., for any task tsk in ts, max_arrival tsk is (1) an arrival bound of tsk, and (2) it is a monotonic function that equals 0 for the empty interval delta = 0.
Context `{MaxArrivals Task}.
Hypothesis H_valid_arrival_curve : valid_taskset_arrival_curve ts max_arrivals.
Further assume we are given a function that generates the required number of jobs of a given task at a given instant of time.
Variable generate_jobs_at : Task → nat → instant → seq Job.
First, we assume that generate_jobs_at tsk n t generates n jobs.
Hypothesis H_job_generation_valid_number :
∀ (tsk : Task) (n : nat) (t : instant), tsk \in ts → size (generate_jobs_at tsk n t) = n.
Second, we assume that generate_jobs_at tsk n t generates jobs of task tsk that arrive at time t.
Hypothesis H_job_generation_valid_jobs :
∀ (tsk : Task) (n : nat) (t : instant) (j : Job),
(j \in generate_jobs_at tsk n t) →
job_task j = tsk
∧ job_arrival j = t
∧ job_cost j ≤ task_cost tsk.
Finally, we assume that all jobs generated by generate_jobs_at are unique.
Hypothesis H_jobs_unique :
∀ (t1 t2 : instant),
uniq (arrivals_between (concrete_arrival_sequence generate_jobs_at ts) t1 t2).
Assuming such a well-behaved "constructor" generate_jobs_at, we prove a few validity claims about an arrival sequence generated by concrete_arrival_sequence.
We start by showing that the obtained arrival sequence is a set.
Lemma arr_seq_is_a_set :
arrival_sequence_uniq (concrete_arrival_sequence generate_jobs_at ts).
Proof.
move⇒ t.
move: (H_jobs_unique t t.+1).
by rewrite /arrivals_between big_nat1.
Qed.
Next, we show that all jobs in the arrival sequence come from ts.
Lemma concrete_all_jobs_from_taskset :
all_jobs_from_taskset (concrete_arrival_sequence generate_jobs_at ts) ts.
Proof.
move⇒ j [t /mem_bigcat_exists [tsk [TSK_IN IN]]].
move: (H_job_generation_valid_jobs tsk _ _ _ IN) ⇒ [JOB_TASK _].
by rewrite JOB_TASK.
Qed.
Further, we note that the jobs in the arrival sequence have consistent arrival times.
Lemma arrival_times_are_consistent :
consistent_arrival_times (concrete_arrival_sequence generate_jobs_at ts).
Proof.
move⇒ j t /mem_bigcat_exists [tsk [TSK_IN IN]].
by move: (H_job_generation_valid_jobs tsk _ _ _ IN) ⇒ [_ [JOB_ARR _]].
Qed.
Lastly, we observe that the jobs in the arrival sequence have valid job costs.
Lemma concrete_valid_job_cost :
arrivals_have_valid_job_costs (concrete_arrival_sequence generate_jobs_at ts).
Proof.
move⇒ j [t /mem_bigcat_exists [tsk [TSK_IN IN]]].
move: (H_job_generation_valid_jobs tsk _ _ _ IN) ⇒ [JOB_TASK [_ JOB_COST]].
by rewrite /valid_job_cost JOB_TASK.
Qed.
In this section, we prove a series of facts regarding the maximal arrival sequence, leading up to the main theorem that all arrival-curve constraints are respected.
Section Facts.
Let tsk be any task in ts that is to be analyzed.
Variable tsk : Task.
Hypothesis H_tsk_in_ts : tsk \in ts.
First, we show that the arrivals at time t are indeed generated by generate_jobs_at applied at time t.
Lemma task_arrivals_at_eq_generate_jobs_at :
∀ t,
task_arrivals_at (concrete_arrival_sequence generate_jobs_at ts) tsk t
= generate_jobs_at tsk (max_arrivals_at tsk t) t.
Proof.
move⇒ t.
rewrite /task_arrivals_at bigcat_filter_eq_filter_bigcat bigcat_seq_uniqK // ⇒ tsk0 j INj.
apply H_job_generation_valid_jobs in INj.
by destruct INj.
Qed.
Next, we show that the number of arrivals at time t always matches max_arrivals_at applied at time t.
Lemma task_arrivals_at_eq :
∀ t,
size (task_arrivals_at (concrete_arrival_sequence generate_jobs_at ts) tsk t)
= max_arrivals_at tsk t.
Proof. by move⇒ t; rewrite task_arrivals_at_eq_generate_jobs_at. Qed.
We then generalize the previous result to an arbitrary interval `[t1,t2)`.
Lemma number_of_task_arrivals_eq :
∀ t1 t2,
number_of_task_arrivals (concrete_arrival_sequence generate_jobs_at ts) tsk t1 t2
= \sum_(t1 ≤ t < t2) max_arrivals_at tsk t.
Proof.
move⇒ t1 t2.
rewrite /number_of_task_arrivals task_arrivals_between_is_cat_of_task_arrivals_at -size_big_nat.
apply eq_big_nat ⇒ t RANGE.
by apply task_arrivals_at_eq.
Qed.
We further show that, starting from an empty prefix and applying extend_arrival_prefix t times, we end up with a prefix of size t...
Lemma extend_horizon_size :
∀ t,
size (iter t (extend_arrival_prefix tsk) [::]) = t.
Proof. by elim⇒ // t IHt; rewrite size_cat IHt //=; lia. Qed.
...and that the arrival sequence prefix up to an arbitrary horizon t is a sequence of t+1 elements.
Lemma prefix_up_to_size :
∀ t,
size (maximal_arrival_prefix tsk t) = t.+1.
Proof.
by elim⇒ // t IHt; rewrite /maximal_arrival_prefix /extend_arrival_prefix size_cat IHt //=; lia.
Qed.
Next, we prove prefix inclusion for maximal_arrival_prefix when the horizon is expanded by one...
Lemma n_arrivals_at_prefix_inclusion1 :
∀ t h,
t ≤ h →
nth 0 (maximal_arrival_prefix tsk h) t
= nth 0 (maximal_arrival_prefix tsk h.+1) t.
Proof.
move⇒ t h LEQ.
rewrite /maximal_arrival_prefix //= {3}/extend_arrival_prefix nth_cat prefix_up_to_size.
by case: (ltnP t h.+1); lia.
Qed.
...and we generalize the previous result to two arbitrary horizons h1 ≤ h2.
Lemma n_arrivals_at_prefix_inclusion :
∀ t h1 h2,
t ≤ h1 ≤ h2 →
nth 0 (maximal_arrival_prefix tsk h1) t = nth 0 (maximal_arrival_prefix tsk h2) t.
Proof.
move⇒ t h1 h2 /andP[LEQh1 LEQh2].
elim: h2 LEQh2 ⇒ [|h2 IHh2] LEQh2; [by have → : h1 = 0; lia |].
rewrite leq_eqVlt in LEQh2.
move: LEQh2 ⇒ /orP [/eqP EQ | LT]; first by rewrite EQ.
feed IHh2; first by lia.
rewrite -n_arrivals_at_prefix_inclusion1 //.
by lia.
Qed.
Next, we prove that, for any positive time instant t, max_arrivals_at indeed matches the arrivals of next_max_arrival applied at t-1.
Lemma max_arrivals_at_next_max_arrivals_eq :
∀ t,
0 < t →
max_arrivals_at tsk t
= next_max_arrival tsk (maximal_arrival_prefix tsk t.-1).
Proof.
move ⇒ t GT0.
move: prefix_up_to_size; rewrite /maximal_arrival_prefix ⇒ PUS.
rewrite /max_arrivals_at /maximal_arrival_prefix {1}/extend_arrival_prefix nth_cat extend_horizon_size //= ltnn //= subnn //=.
by destruct t.
Qed.
Given a time instant t and interval Δ, we show that max_arrivals_at applied at time t is always less-or-equal to max_arrivals applied to Δ+1, even when each value of max_arrivals_at in the interval `[t-Δ, t)` is subtracted from it.
Lemma n_arrivals_at_leq :
∀ t Δ,
Δ ≤ t →
max_arrivals_at tsk t
≤ max_arrivals tsk Δ.+1 - \sum_(t - Δ ≤ i < t) max_arrivals_at tsk i.
Proof.
move⇒ t Δ LEQ.
move: (H_valid_arrival_curve tsk H_tsk_in_ts) ⇒ [ZERO MONO].
destruct t as [|t].
{ rewrite unlock //= subn0.
rewrite /max_arrivals_at /maximal_arrival_prefix /extend_arrival_prefix
/next_max_arrival //= /suffix_sum subn0 unlock subn0.
by apply MONO. }
{ rewrite max_arrivals_at_next_max_arrivals_eq; last by done.
rewrite /next_max_arrival /jobs_remaining prefix_up_to_size.
simpl (t.+1.-1).
destruct supremum eqn:SUP; last by move:(supremum_none _ _ SUP); rewrite map_cons.
eapply (supremum_spec _ leqnn leq_total leq_trans _ _ SUP).
rewrite /suffix_sum prefix_up_to_size /max_arrivals_at.
have → : \sum_(t.+1 - Δ ≤ i < t.+1) nth 0 (maximal_arrival_prefix tsk i) i
= \sum_(t.+1 - Δ ≤ i < t.+1) nth 0 (maximal_arrival_prefix tsk t) i.
{ apply eq_big_nat ⇒ i RANGE.
by apply n_arrivals_at_prefix_inclusion; lia. }
set f := fun x ⇒ max_arrivals _ x.+1 - \sum_(t.+1-x ≤ i < t.+1) nth 0 (maximal_arrival_prefix _ t) i.
have→ : max_arrivals tsk Δ.+1 - \sum_(t.+1 - Δ ≤ i < t.+1) nth 0 (maximal_arrival_prefix tsk t) i = f Δ by done.
apply map_f.
by rewrite mem_iota; lia. }
Qed.
End Facts.
Finally, we prove our main result, that is, the proposed maximal arrival sequence instantiation indeed respects all arrival-curve constraints.
Theorem concrete_is_arrival_curve :
taskset_respects_max_arrivals (concrete_arrival_sequence generate_jobs_at ts) ts.
Proof.
move⇒ tsk IN t1 t.
have [LEQ|LT] := leqP t1 t.
- set Δ := t - t1.
replace t1 with (t - Δ); last by rewrite /Δ; lia.
have LEQd: Δ ≤ t by lia.
generalize Δ LEQd; clear LEQ Δ LEQd.
elim: t ⇒ [|t IHt] Δ LEQd.
{ rewrite sub0n.
rewrite number_of_task_arrivals_eq //.
by vm_compute; rewrite unlock. }
{ rewrite number_of_task_arrivals_eq //.
destruct Δ as [|Δ]; first by rewrite /index_iota subnn; vm_compute; rewrite unlock.
rewrite subSS.
specialize (IHt Δ).
feed IHt; first by lia.
rewrite number_of_task_arrivals_eq // in IHt.
rewrite big_nat_recr //=; last by lia.
rewrite -leq_subRL; first apply n_arrivals_at_leq; try lia.
move: (H_valid_arrival_curve tsk IN) ⇒ [ZERO MONO].
apply (leq_trans IHt).
by apply MONO. }
- rewrite /number_of_task_arrivals /task_arrivals_between.
rewrite arrivals_between_geq; last by lia.
by [].
Qed.
End MaximalArrivalSequence.