# 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).
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.
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).
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).
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.
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.
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.
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.
...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.
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.
...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.
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).
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.
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.
End MaximalArrivalSequence.