# Library prosa.implementation.refinements.arrival_bound

In this section, we define a generic version of arrival bound and prove that it is isomorphic to the standard, natural-number-based definition.
Section Definitions.

Consider a generic type T, for which all the basic arithmetical operations, ordering, and equality are defined.
Context {T : Type}.
Context `{!zero_of T, !one_of T, !sub_of T, !add_of T, !mul_of T,
!div_of T, !mod_of T, !eq_of T, !leq_of T, !lt_of T}.
Context `{!eq_of (seq T)}.
Context `{!eq_of (T × seq (T × T))}.

As in the natural-numbers-based definition, an arrival curve prefix is composed of an horizon and a list of steps.
Let ArrivalCurvePrefix : Type := T × seq (T × T).

A task's arrival bound is an inductive type comprised of three types of arrival patterns: (a) periodic, characterized by a period between consequent activation of a task, (b) sporadic, characterized by a minimum inter-arrival time, or (c) arrival-curve prefix, characterized by a finite prefix of an arrival curve.
Further, we define the equality for two generic tasks as the equality of each attribute.
match tb1, tb2 with
| Periodic_T p1, Periodic_T p2 ⇒ (p1 == p2)%C
| ArrivalPrefix_T s1, ArrivalPrefix_T s2 ⇒ (s1 == s2)%C
| _, _false
end.

The first component of arrival-curve prefix ac_prefix is called horizon.
Definition horizon_of_T (ac_prefix_vec : T × seq (T × T)) := fst ac_prefix_vec.

The second component of ac_prefix is called steps.
Definition steps_of_T (ac_prefix_vec : T × seq (T × T)) := snd ac_prefix_vec.

The time steps of ac_prefix are the first components of the steps. That is, these are time instances before the horizon where the corresponding arrival curve makes a step.
The function step_at returns the last step (duration × value) such that duration t.
Definition step_at_T (ac_prefix_vec : T × seq (T × T)) (t : T) :=
(last (0, 0) [ seq step <- steps_of_T ac_prefix_vec | fst step t ])%C.

The function value_at returns the value of the last step (duration × value) such that duration t
Definition value_at_T (ac_prefix_vec : T × seq (T × T)) (t : T) := snd (step_at_T ac_prefix_vec t).

Finally, we define a generic version of the function extrapolated_arrival_curve that performs the periodic extension of the arrival-curve prefix (and hence, defines an arrival curve).
Definition extrapolated_arrival_curve_T (ac_prefix_vec : T × seq (T × T)) (t : T) :=
let h := horizon_of_T ac_prefix_vec in
(t %/ h × value_at_T ac_prefix_vec h + value_at_T ac_prefix_vec (t %% h))%C.

Steps should be strictly increasing both in time steps and values.
Definition ltn_steps_T (a b : T × T) := (fst a < fst b)%C && (snd a < snd b)%C.
Definition sorted_ltn_steps_T (ac_prefix : ArrivalCurvePrefix) :=
sorted ltn_steps_T (steps_of_T ac_prefix).

We also define a predicate for non-decreasing order that is more convenient for proving some of the claims.
Definition leq_steps_T (a b : T × T) := (fst a fst b)%C && (snd a snd b)%C.

Horizon should be positive.
Horizon should bound time steps.
There should be no infinite arrivals; that is, value_at 0 = 0.
Definition no_inf_arrivals_T (ac_prefix : ArrivalCurvePrefix) :=
(value_at_T ac_prefix 0 == 0)%C.

Bursts must be specified; that is, steps_of should contain a pair (ε, b).
Definition specified_bursts_T (ac_prefix : ArrivalCurvePrefix) :=
has (fun stepstep == 1)%C (time_steps_of_T ac_prefix).

The conjunction of the 5 afore-defined properties defines a valid arrival-curve prefix.
First, we define the function that maps a generic arrival-curve prefix to a natural-number one...
... and its function relationship.
Definition RArrivalCurvePrefix := fun_hrel ACPrefixT_to_ACPrefix.

Next, we define the converse function, mapping a natural-number arrival-curve prefix task to a generic one.
Further, we define the function that maps a generic task arrival-bound to a natural-number one...
match ab with
| Periodic_T pPeriodic p
| ArrivalPrefix_T ac_prefix_vecArrivalPrefix (ACPrefixT_to_ACPrefix ac_prefix_vec)
end.

... and its function relationship.

Finally, we define the converse function, mapping a natural-number task arrival-bound task to a generic one.
match ab with
| Periodic pPeriodic_T (bin_of_nat p)
| ArrivalPrefix ac_prefix_vecArrivalPrefix_T (ACPrefix_to_ACPrefixT ac_prefix_vec)
end.

End Translation.

Section Lemmas.

We prove that leq_steps_T is transitive...
Lemma leq_stepsT_is_transitive:
transitive (@leq_steps_T N leq_N).

... and so is ltn_steps_T.
Lemma ltn_stepsT_is_transitive:
transitive (@ltn_steps_T N lt_N).

End Lemmas.

In this fairly technical section, we prove a series of refinements aimed to be able to convert between a standard natural-number task and a generic task.
Section Refinements.

We prove the refinement for the leq_steps function.
Global Instance refine_leq_steps :
refines (prod_R Rnat Rnat ==> prod_R Rnat Rnat ==> bool_R)%rel leq_steps leq_steps_T.

Next, we prove the refinement for the ltn_steps function.
Global Instance refine_ltn_steps :
refines (prod_R Rnat Rnat ==> prod_R Rnat Rnat ==> bool_R)%rel ltn_steps ltn_steps_T.

Next, we prove the refinement for the ACPrefixT_to_ACPrefix function.

Next, we prove the refinement for the ltn_steps_sorted function.
Global Instance refine_ltn_steps_sorted :
xs xs',
refines ( list_R (prod_R Rnat Rnat) )%rel xs xs'
refines ( bool_R )%rel (sorted ltn_steps xs) (sorted ltn_steps_T xs').

Next, we prove the refinement for the leq_steps_sorted function.
Global Instance refine_leq_steps_sorted :
xs xs',
refines ( list_R (prod_R Rnat Rnat) )%rel xs xs'
refines ( bool_R )%rel (sorted leq_steps xs) (sorted leq_steps_T xs').

Next, we prove the refinement for the value_at function.
Global Instance refine_value_at :
refines (prod_R Rnat (list_R (prod_R Rnat Rnat)) ==> Rnat ==> Rnat)%rel value_at value_at_T.

Next, we prove the refinement for the time_steps_of function.
Global Instance refine_get_time_steps :
refines (prod_R Rnat (list_R (prod_R Rnat Rnat)) ==> list_R Rnat)%rel time_steps_of time_steps_of_T.

Next, we prove the refinement for the extrapolated_arrival_curve function.
Global Instance refine_arrival_curve_prefix :
refines (prod_R Rnat (list_R (prod_R Rnat Rnat)) ==> Rnat ==> Rnat)%rel extrapolated_arrival_curve extrapolated_arrival_curve_T.

Next, we prove the refinement for the ArrivalCurvePrefix function.
Global Instance refine_ArrivalPrefix:
refines (prod_R Rnat (list_R (prod_R Rnat Rnat)) ==> Rtask_ab)%rel ArrivalPrefix ArrivalPrefix_T.

Next, we define some useful equality functions to guide the typeclass engine.
Global Instance eq_listN : eq_of (seq N) := fun x yx == y.
Global Instance eq_NlistNN : eq_of (prod N (seq (prod N N))) := fun x yx == y.