Built with
Alectryon , running Coq+SerAPI v8.19.0+0.19.0. Bubbles (
) indicate interactive fragments: hover for details, tap to reveal contents. Use
Ctrl+↑ Ctrl+↓ to navigate,
Ctrl+🖱️ to focus. On Mac, use
⌘ instead of
Ctrl .
Require Export prosa.analysis.definitions.request_bound_function.[Loading ML file ssrmatching_plugin.cmxs (using legacy method) ... done ] [Loading ML file ssreflect_plugin.cmxs (using legacy method) ... done ] [Loading ML file ring_plugin.cmxs (using legacy method) ... done ] [Loading ML file coq-elpi.elpi ... done ] [Loading ML file zify_plugin.cmxs (using legacy method) ... done ] [Loading ML file micromega_plugin.cmxs (using legacy method) ... done ] [Loading ML file btauto_plugin.cmxs (using legacy method) ... done ] Notation "_ + _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ - _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ <= _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ < _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ >= _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ > _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ <= _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing,default]Notation "_ < _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing,default]Notation "_ <= _ < _" was already used in scope
nat_scope. [notation-overridden,parsing,default]Notation "_ < _ < _" was already used in scope
nat_scope. [notation-overridden,parsing,default]Notation "_ * _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Require Export prosa.implementation.refinements.task.[Loading ML file paramcoq.cmxs (using legacy method) ... done ]
(** ** Arrival Curve Refinements. *)
(** In this module, we provide a series of definitions related to arrival curves
when working with generic tasks. *)
(** First, we define a helper function that yields the horizon of the arrival
curve prefix of a task ... *)
Definition get_horizon_of_task (tsk : Task) : duration :=
horizon_of (get_arrival_curve_prefix tsk).
(** ... another one that yields the time steps of the arrival curve, ... *)
Definition get_time_steps_of_task (tsk : Task) : seq duration :=
time_steps_of (get_arrival_curve_prefix tsk).
(** ... a function that yields the same time steps, offset by δ, ...**)
Definition time_steps_with_offset tsk δ := [seq t + δ | t <- get_time_steps_of_task tsk].
(** ... and a generalization of the previous function that repeats the time
steps for each given offset. *)
Definition repeat_steps_with_offset (tsk : Task) (offsets : seq nat): seq nat :=
flatten (map (time_steps_with_offset tsk) offsets).
(** For convenience, we provide a short form to indicate the request-bound
function of a task. *)
Definition task_rbf (tsk : Task) (Δ : duration) :=
task_request_bound_function tsk Δ.
(** Further, we define a valid arrival bound as (1) a positive
minimum inter-arrival time/period, or (2) a valid arrival curve prefix. *)
Definition valid_arrivals (tsk : Task) : bool :=
match task_arrival tsk with
| Periodic p => p >= 1
| Sporadic m => m >= 1
| ArrivalPrefix emax_vec => valid_arrival_curve_prefix_dec emax_vec
end .
(** Next, we define some helper functions, that indicate whether
the given task is periodic, ... *)
Definition is_periodic_arrivals (tsk : Task) : Prop :=
exists p , task_arrival tsk = Periodic p.
(** ... sporadic, ... *)
Definition is_sporadic_arrivals (tsk : Task) : Prop :=
exists m , task_arrival tsk = Sporadic m.
(** ... or bounded by an arrival curve. *)
Definition is_etamax_arrivals (tsk : Task) : Prop :=
exists ac_prefix_vec , task_arrival tsk = ArrivalPrefix ac_prefix_vec.
(** Further, for convenience, we define the notion of task
having a valid arrival curve. *)
Definition has_valid_arrival_curve_prefix (tsk : Task) :=
exists ac_prefix_vec , get_arrival_curve_prefix tsk = ac_prefix_vec /\
valid_arrival_curve_prefix ac_prefix_vec.
(** Finally, we define define the notion of task set with
valid arrivals. *)
Definition task_set_with_valid_arrivals (ts : seq Task) :=
forall tsk ,
tsk \in ts -> valid_arrivals tsk.
(** In this section, we prove some facts regarding the above definitions. *)
Section Facts .
(** Consider a task [tsk]. *)
Variable tsk : Task.
(** We show that a task is either periodic, sporadic, or bounded by
an arrival-curve prefix. *)
Lemma arrival_cases :
is_periodic_arrivals tsk
\/ is_sporadic_arrivals tsk
\/ is_etamax_arrivals tsk.tsk : Task
is_periodic_arrivals tsk \/
is_sporadic_arrivals tsk \/ is_etamax_arrivals tsk
Proof .tsk : Task
is_periodic_arrivals tsk \/
is_sporadic_arrivals tsk \/ is_etamax_arrivals tsk
rewrite /is_periodic_arrivals /is_sporadic_arrivals /is_etamax_arrivals.tsk : Task
(exists p : nat, task_arrival tsk = Periodic p) \/
(exists m : nat, task_arrival tsk = Sporadic m) \/
(exists ac_prefix_vec : ArrivalCurvePrefix,
task_arrival tsk = ArrivalPrefix ac_prefix_vec)
destruct (task_arrival tsk).tsk : Task n : nat
(exists p : nat, Periodic n = Periodic p) \/
(exists m : nat, Periodic n = Sporadic m) \/
(exists ac_prefix_vec : ArrivalCurvePrefix,
Periodic n = ArrivalPrefix ac_prefix_vec)
- tsk : Task n : nat
(exists p : nat, Periodic n = Periodic p) \/
(exists m : nat, Periodic n = Sporadic m) \/
(exists ac_prefix_vec : ArrivalCurvePrefix,
Periodic n = ArrivalPrefix ac_prefix_vec)
by left ; eexists ; reflexivity .
- tsk : Task n : nat
(exists p : nat, Sporadic n = Periodic p) \/
(exists m : nat, Sporadic n = Sporadic m) \/
(exists ac_prefix_vec : ArrivalCurvePrefix,
Sporadic n = ArrivalPrefix ac_prefix_vec)
by right ; left ; eexists ; reflexivity .
- tsk : Task a : ArrivalCurvePrefix
(exists p : nat, ArrivalPrefix a = Periodic p) \/
(exists m : nat, ArrivalPrefix a = Sporadic m) \/
(exists ac_prefix_vec : ArrivalCurvePrefix,
ArrivalPrefix a = ArrivalPrefix ac_prefix_vec)
by right ; right ; eexists ; reflexivity .
Qed .
End Facts .
(** In this fairly technical section, we prove a series of refinements
aimed to be able to convert between a standard natural-number task
arrival bound and an arrival bound that uses, instead of numbers,
a generic type [T]. *)
Section Theory .
(** First, we prove a refinement for [positive_horizon]. *)
Local Instance refine_positive_horizon :
refines (prod_R Rnat (list_R (prod_R Rnat Rnat)) ==> bool_R)%rel
positive_horizon positive_horizon_T.refines
(prod_R Rnat (list_R (prod_R Rnat Rnat)) ==> bool_R)
positive_horizon positive_horizon_T
Proof .refines
(prod_R Rnat (list_R (prod_R Rnat Rnat)) ==> bool_R)
positive_horizon positive_horizon_T
unfold positive_horizon, positive_horizon_T.refines
(prod_R Rnat (list_R (prod_R Rnat Rnat)) ==> bool_R)
(fun ac_prefix : ArrivalCurvePrefix =>
0 < horizon_of ac_prefix)
(fun
ac_prefix : binnat.N * seq (binnat.N * binnat.N)
=> (0 < horizon_of_T ac_prefix)%C)
apply : refines_abstr => a b X.a : (nat * seq (nat * nat))%type b : (binnat.N * seq (binnat.N * binnat.N))%type X : refines (prod_R Rnat (list_R (prod_R Rnat Rnat)))
a b
refines bool_R (0 < horizon_of a)
(0 < horizon_of_T b)%C
unfold horizon_of, horizon_of_T.a : (nat * seq (nat * nat))%type b : (binnat.N * seq (binnat.N * binnat.N))%type X : refines (prod_R Rnat (list_R (prod_R Rnat Rnat)))
a b
refines bool_R (0 < a.1 ) (0 < b.1 )%C
destruct a as [h s], b as [h' s']; simpl .h : nat s : seq (nat * nat) h' : binnat.N s' : seq (binnat.N * binnat.N) X : refines (prod_R Rnat (list_R (prod_R Rnat Rnat)))
(h, s) (h', s')
refines bool_R (0 < h) (0 < h')%C
rewrite refinesE; rewrite refinesE in X; inversion_clear X.h : nat s : seq (nat * nat) h' : binnat.N s' : seq (binnat.N * binnat.N) a_R : Rnat h h' b_R : list_R (prod_R Rnat Rnat) s s'
bool_R (0 < h) (0 < h')%C
by apply refine_ltn; auto using Rnat_0.
Qed .
(** Next, we prove a refinement for [large_horizon]. *)
Local Instance refine_large_horizon :
refines (prod_R Rnat (list_R (prod_R Rnat Rnat)) ==> bool_R)%rel
large_horizon_dec large_horizon_T.refines
(prod_R Rnat (list_R (prod_R Rnat Rnat)) ==> bool_R)
large_horizon_dec large_horizon_T
Proof .refines
(prod_R Rnat (list_R (prod_R Rnat Rnat)) ==> bool_R)
large_horizon_dec large_horizon_T
unfold large_horizon_dec, large_horizon_T.refines
(prod_R Rnat (list_R (prod_R Rnat Rnat)) ==> bool_R)
(fun ac_prefix : ArrivalCurvePrefix =>
all (leq^~ (horizon_of ac_prefix))
(time_steps_of ac_prefix))
(fun
ac_prefix : binnat.N * seq (binnat.N * binnat.N)
=>
all (leq_op^~ (horizon_of_T ac_prefix))
(time_steps_of_T ac_prefix))
apply refines_abstr; intros ac ac' Rac.ac : (nat * seq (nat * nat))%type ac' : (binnat.N * seq (binnat.N * binnat.N))%type Rac : refines (prod_R Rnat (list_R (prod_R Rnat Rnat))) ac ac'
refines bool_R
(all (leq^~ (horizon_of ac)) (time_steps_of ac))
(all (leq_op^~ (horizon_of_T ac'))
(time_steps_of_T ac'))
refines_apply. ac : (nat * seq (nat * nat))%type ac' : (binnat.N * seq (binnat.N * binnat.N))%type Rac : refines (prod_R Rnat (list_R (prod_R Rnat Rnat))) ac ac'
refines (Rnat ==> bool_R) (leq^~ (horizon_of ac))
(leq_op^~ (horizon_of_T ac'))
apply refines_abstr; intros a a' Ra.ac : (nat * seq (nat * nat))%type ac' : (binnat.N * seq (binnat.N * binnat.N))%type Rac : refines (prod_R Rnat (list_R (prod_R Rnat Rnat))) ac ac' a : nat a' : binnat.N Ra : refines Rnat a a'
refines bool_R (a <= horizon_of ac)
(a' <= horizon_of_T ac')%C
by refines_apply.
Qed .
(** Next, we prove a refinement for [no_inf_arrivals]. *)
Local Instance refine_no_inf_arrivals :
refines (prod_R Rnat (list_R (prod_R Rnat Rnat)) ==> bool_R)%rel
no_inf_arrivals no_inf_arrivals_T.refines
(prod_R Rnat (list_R (prod_R Rnat Rnat)) ==> bool_R)
no_inf_arrivals no_inf_arrivals_T
Proof .refines
(prod_R Rnat (list_R (prod_R Rnat Rnat)) ==> bool_R)
no_inf_arrivals no_inf_arrivals_T
unfold no_inf_arrivals, no_inf_arrivals_T.refines
(prod_R Rnat (list_R (prod_R Rnat Rnat)) ==> bool_R)
(fun ac_prefix : ArrivalCurvePrefix =>
value_at ac_prefix 0 == 0 )
(fun
ac_prefix : binnat.N * seq (binnat.N * binnat.N)
=> (value_at_T ac_prefix 0 == 0 )%C)
apply refines_abstr; intros ac ac' Rac.ac : (nat * seq (nat * nat))%type ac' : (binnat.N * seq (binnat.N * binnat.N))%type Rac : refines (prod_R Rnat (list_R (prod_R Rnat Rnat))) ac ac'
refines bool_R (value_at ac 0 == 0 )
(value_at_T ac' 0 == 0 )%C
refines_apply.
Qed .
(** Next, we prove a refinement for [specified_bursts]. *)
Local Instance refine_specified_bursts :
refines (prod_R Rnat (list_R (prod_R Rnat Rnat)) ==> bool_R)%rel
specified_bursts specified_bursts_T.refines
(prod_R Rnat (list_R (prod_R Rnat Rnat)) ==> bool_R)
specified_bursts specified_bursts_T
Proof .refines
(prod_R Rnat (list_R (prod_R Rnat Rnat)) ==> bool_R)
specified_bursts specified_bursts_T
unfold specified_bursts, specified_bursts_T.refines
(prod_R Rnat (list_R (prod_R Rnat Rnat)) ==> bool_R)
(fun ac_prefix : ArrivalCurvePrefix =>
1 \in time_steps_of ac_prefix)
(fun
ac_prefix : binnat.N * seq (binnat.N * binnat.N)
=>
has (Refinements.Op.eq_op^~ 1 %C)
(time_steps_of_T ac_prefix))
apply refines_abstr; intros ac ac' Rac.ac : (nat * seq (nat * nat))%type ac' : (binnat.N * seq (binnat.N * binnat.N))%type Rac : refines (prod_R Rnat (list_R (prod_R Rnat Rnat))) ac ac'
refines bool_R (1 \in time_steps_of ac)
(has (Refinements.Op.eq_op^~ 1 %C)
(time_steps_of_T ac'))
rewrite -has_pred1.ac : (nat * seq (nat * nat))%type ac' : (binnat.N * seq (binnat.N * binnat.N))%type Rac : refines (prod_R Rnat (list_R (prod_R Rnat Rnat))) ac ac'
refines bool_R (has (pred1 1 ) (time_steps_of ac))
(has (Refinements.Op.eq_op^~ 1 %C)
(time_steps_of_T ac'))
refines_apply; last first . ac : (nat * seq (nat * nat))%type ac' : (binnat.N * seq (binnat.N * binnat.N))%type Rac : refines (prod_R Rnat (list_R (prod_R Rnat Rnat))) ac ac'
refines ?R (pred1 1 ) (Refinements.Op.eq_op^~ 1 %C)
- ac : (nat * seq (nat * nat))%type ac' : (binnat.N * seq (binnat.N * binnat.N))%type Rac : refines (prod_R Rnat (list_R (prod_R Rnat Rnat))) ac ac'
refines ?R (pred1 1 ) (Refinements.Op.eq_op^~ 1 %C)
by refines_abstr; rewrite pred1E eq_sym ; refines_apply.
- ac : (nat * seq (nat * nat))%type ac' : (binnat.N * seq (binnat.N * binnat.N))%type Rac : refines (prod_R Rnat (list_R (prod_R Rnat Rnat))) ac ac'
refines ((Rnat ==> bool_R) ==> list_R Rnat ==> bool_R)
has has
refines_abstr. ac : (nat * seq (nat * nat))%type ac' : (binnat.N * seq (binnat.N * binnat.N))%type Rac : refines (prod_R Rnat (list_R (prod_R Rnat Rnat))) ac ac' _a_ : pred Datatypes_nat__canonical__eqtype_Equality _b_ : pred binnat.N _Hyp_ : refines (Rnat ==> bool_R) _a_ _b_ _a1_ : seq Datatypes_nat__canonical__eqtype_Equality _b1_ : seq binnat.N _Hyp1_ : refines (list_R Rnat) _a1_ _b1_
refines bool_R (has _a_ _a1_) (has _b_ _b1_)
rewrite refinesE; eapply has_R; last by apply refinesP; eassumption .ac : (nat * seq (nat * nat))%type ac' : (binnat.N * seq (binnat.N * binnat.N))%type Rac : refines (prod_R Rnat (list_R (prod_R Rnat Rnat))) ac ac' _a_ : pred Datatypes_nat__canonical__eqtype_Equality _b_ : pred binnat.N _Hyp_ : refines (Rnat ==> bool_R) _a_ _b_ _a1_ : seq Datatypes_nat__canonical__eqtype_Equality _b1_ : seq binnat.N _Hyp1_ : refines (list_R Rnat) _a1_ _b1_
forall
(t₁ : Datatypes_nat__canonical__eqtype_Equality)
(t₂ : binnat.N),
Rnat t₁ t₂ -> bool_R (_a_ t₁) (_b_ t₂)
by intros ; apply refinesP; refines_apply.
Qed .
(** Next, we prove a refinement for the arrival curve prefix validity. *)
Local Instance refine_valid_arrival_curve_prefix :
refines
(prod_R Rnat (list_R (prod_R Rnat Rnat)) ==> bool_R)%rel
valid_arrival_curve_prefix_dec
valid_extrapolated_arrival_curve_T.refines
(prod_R Rnat (list_R (prod_R Rnat Rnat)) ==> bool_R)
valid_arrival_curve_prefix_dec
valid_extrapolated_arrival_curve_T
Proof .refines
(prod_R Rnat (list_R (prod_R Rnat Rnat)) ==> bool_R)
valid_arrival_curve_prefix_dec
valid_extrapolated_arrival_curve_T
apply refines_abstr.forall (a : nat * seq (nat * nat))
(b : binnat.N * seq (binnat.N * binnat.N)),
refines (prod_R Rnat (list_R (prod_R Rnat Rnat))) a b ->
refines bool_R (valid_arrival_curve_prefix_dec a)
(valid_extrapolated_arrival_curve_T b)
unfold valid_arrival_curve_prefix_dec, valid_extrapolated_arrival_curve_T.forall (a : nat * seq (nat * nat))
(b : binnat.N * seq (binnat.N * binnat.N)),
refines (prod_R Rnat (list_R (prod_R Rnat Rnat))) a b ->
refines bool_R
(positive_horizon a && large_horizon_dec a &&
no_inf_arrivals a && specified_bursts a &&
sorted_ltn_steps a)
(positive_horizon_T b && large_horizon_T b &&
no_inf_arrivals_T b && specified_bursts_T b &&
sorted_ltn_steps_T b)
by intros ; refines_apply.
Qed .
(** Next, we prove a refinement for the arrival curve validity. *)
Global Instance refine_valid_arrivals :
forall tsk ,
refines (bool_R)%rel
(valid_arrivals (taskT_to_task tsk))
(valid_arrivals_T tsk) | 0 .forall tsk : task_T,
refines bool_R (valid_arrivals (taskT_to_task tsk))
(valid_arrivals_T tsk)
Proof .forall tsk : task_T,
refines bool_R (valid_arrivals (taskT_to_task tsk))
(valid_arrivals_T tsk)
move => tsk.tsk : task_T
refines bool_R (valid_arrivals (taskT_to_task tsk))
(valid_arrivals_T tsk)
have Rtsk := refine_task'.tsk : task_T Rtsk : refines (unify (A:=task_T) ==> Rtask)
taskT_to_task id
refines bool_R (valid_arrivals (taskT_to_task tsk))
(valid_arrivals_T tsk)
rewrite refinesE in Rtsk.tsk : task_T Rtsk : (unify (A:=task_T) ==> Rtask)%rel taskT_to_task
id
refines bool_R (valid_arrivals (taskT_to_task tsk))
(valid_arrivals_T tsk)
specialize (Rtsk tsk tsk (unifyxx _)); simpl in Rtsk.tsk : task_T Rtsk : Rtask (taskT_to_task tsk) tsk
refines bool_R (valid_arrivals (taskT_to_task tsk))
(valid_arrivals_T tsk)
have Rab := refine_task_arrival.tsk : task_T Rtsk : Rtask (taskT_to_task tsk) tsk Rab : refines (Rtask ==> Rtask_ab) task_arrival
task_arrival_T
refines bool_R (valid_arrivals (taskT_to_task tsk))
(valid_arrivals_T tsk)
rewrite refinesE in Rab.tsk : task_T Rtsk : Rtask (taskT_to_task tsk) tsk Rab : (Rtask ==> Rtask_ab)%rel task_arrival
task_arrival_T
refines bool_R (valid_arrivals (taskT_to_task tsk))
(valid_arrivals_T tsk)
specialize (Rab _ _ Rtsk).tsk : task_T Rtsk : Rtask (taskT_to_task tsk) tsk Rab : Rtask_ab (task_arrival (taskT_to_task tsk))
(task_arrival_T tsk)
refines bool_R (valid_arrivals (taskT_to_task tsk))
(valid_arrivals_T tsk)
all : unfold valid_arrivals, valid_arrivals_T.tsk : task_T Rtsk : Rtask (taskT_to_task tsk) tsk Rab : Rtask_ab (task_arrival (taskT_to_task tsk))
(task_arrival_T tsk)
refines bool_R
match task_arrival (taskT_to_task tsk) with
| Periodic p => 0 < p
| Sporadic m => 0 < m
| ArrivalPrefix emax_vec =>
valid_arrival_curve_prefix_dec emax_vec
end
match task_arrival_T tsk with
| Periodic_T p => (1 <= p)%C
| Sporadic_T m => (1 <= m)%C
| ArrivalPrefix_T ac_prefix_vec =>
valid_extrapolated_arrival_curve_T ac_prefix_vec
end
destruct (task_arrival (_ _)) as [?|?|arrival_curve_prefix], (task_arrival_T _) as [?|?|arrival_curve_prefixT].tsk : task_T Rtsk : Rtask (taskT_to_task tsk) tsk n : nat n0 : binnat.N Rab : Rtask_ab (Periodic n) (Periodic_T n0)
refines bool_R (0 < n) (1 <= n0)%C
all : try (inversion Rab; fail ).tsk : task_T Rtsk : Rtask (taskT_to_task tsk) tsk n : nat n0 : binnat.N Rab : Rtask_ab (Periodic n) (Periodic_T n0)
refines bool_R (0 < n) (1 <= n0)%C
all : try (refines_apply; rewrite refinesE; inversion Rab; subst ; by done ).tsk : task_T Rtsk : Rtask (taskT_to_task tsk) tsk arrival_curve_prefix : ArrivalCurvePrefix arrival_curve_prefixT : (binnat.N *
seq (binnat.N * binnat.N))%type Rab : Rtask_ab (ArrivalPrefix arrival_curve_prefix)
(ArrivalPrefix_T arrival_curve_prefixT)
refines bool_R
(valid_arrival_curve_prefix_dec arrival_curve_prefix)
(valid_extrapolated_arrival_curve_T
arrival_curve_prefixT)
{ tsk : task_T Rtsk : Rtask (taskT_to_task tsk) tsk arrival_curve_prefix : ArrivalCurvePrefix arrival_curve_prefixT : (binnat.N *
seq (binnat.N * binnat.N))%type Rab : Rtask_ab (ArrivalPrefix arrival_curve_prefix)
(ArrivalPrefix_T arrival_curve_prefixT)
refines bool_R
(valid_arrival_curve_prefix_dec arrival_curve_prefix)
(valid_extrapolated_arrival_curve_T
arrival_curve_prefixT)
unfold ArrivalCurvePrefix in *.tsk : task_T Rtsk : Rtask (taskT_to_task tsk) tsk arrival_curve_prefix : (duration *
seq (duration * nat))%type arrival_curve_prefixT : (binnat.N *
seq (binnat.N * binnat.N))%type Rab : Rtask_ab (ArrivalPrefix arrival_curve_prefix)
(ArrivalPrefix_T arrival_curve_prefixT)
refines bool_R
(valid_arrival_curve_prefix_dec arrival_curve_prefix)
(valid_extrapolated_arrival_curve_T
arrival_curve_prefixT)
refines_apply. tsk : task_T Rtsk : Rtask (taskT_to_task tsk) tsk arrival_curve_prefix : (duration *
seq (duration * nat))%type arrival_curve_prefixT : (binnat.N *
seq (binnat.N * binnat.N))%type Rab : Rtask_ab (ArrivalPrefix arrival_curve_prefix)
(ArrivalPrefix_T arrival_curve_prefixT)
refines (prod_R Rnat (list_R (prod_R Rnat Rnat)))
arrival_curve_prefix arrival_curve_prefixT
destruct arrival_curve_prefix as [h st], arrival_curve_prefixT as [h' st'].tsk : task_T Rtsk : Rtask (taskT_to_task tsk) tsk h : duration st : seq (duration * nat) h' : binnat.N st' : seq (binnat.N * binnat.N) Rab : Rtask_ab (ArrivalPrefix (h, st))
(ArrivalPrefix_T (h', st'))
refines (prod_R Rnat (list_R (prod_R Rnat Rnat)))
(h, st) (h', st')
inversion Rab as [(H0, H1)]; refines_apply.tsk : task_T Rtsk : Rtask (taskT_to_task tsk) tsk h : duration st : seq (duration * nat) h' : binnat.N st' : seq (binnat.N * binnat.N) Rab : Rtask_ab (ArrivalPrefix (h, st))
(ArrivalPrefix_T (h', st')) H0 : h' = h H1 : m_tb2tn st' = st
refines (list_R (prod_R Rnat Rnat)) (m_tb2tn st') st'
rewrite refinesE.tsk : task_T Rtsk : Rtask (taskT_to_task tsk) tsk h : duration st : seq (duration * nat) h' : binnat.N st' : seq (binnat.N * binnat.N) Rab : Rtask_ab (ArrivalPrefix (h, st))
(ArrivalPrefix_T (h', st')) H0 : h' = h H1 : m_tb2tn st' = st
list_R (prod_R Rnat Rnat) (m_tb2tn st') st'
move : H1; clear ; elim : st st' => [|s st IHst] [|s' st'] //.m_tb2tn [::] = [::] ->
list_R (prod_R Rnat Rnat) (m_tb2tn [::]) [::]
- m_tb2tn [::] = [::] ->
list_R (prod_R Rnat Rnat) (m_tb2tn [::]) [::]
by move => _; apply : list_R_nil_R.
- s : (duration * nat)%type st : seq (duration * nat) IHst : forall st' : seq (binnat.N * binnat.N),
m_tb2tn st' = st ->
list_R (prod_R Rnat Rnat) (m_tb2tn st') st's' : (binnat.N * binnat.N)%type st' : seq (binnat.N * binnat.N)
m_tb2tn (s' :: st') = s :: st ->
list_R (prod_R Rnat Rnat) (m_tb2tn (s' :: st'))
(s' :: st')
move => H1; inversion H1 as [(H0, H2)].s : (duration * nat)%type st : seq (duration * nat) IHst : forall st' : seq (binnat.N * binnat.N),
m_tb2tn st' = st ->
list_R (prod_R Rnat Rnat) (m_tb2tn st') st's' : (binnat.N * binnat.N)%type st' : seq (binnat.N * binnat.N) H1 : m_tb2tn (s' :: st') = s :: st H0 : tb2tn s' = s H2 : m_tb2tn st' = st
list_R (prod_R Rnat Rnat) (m_tb2tn (s' :: st'))
(s' :: st')
apply : list_R_cons_R; last by apply IHst.s : (duration * nat)%type st : seq (duration * nat) IHst : forall st' : seq (binnat.N * binnat.N),
m_tb2tn st' = st ->
list_R (prod_R Rnat Rnat) (m_tb2tn st') st's' : (binnat.N * binnat.N)%type st' : seq (binnat.N * binnat.N) H1 : m_tb2tn (s' :: st') = s :: st H0 : tb2tn s' = s H2 : m_tb2tn st' = st
prod_R Rnat Rnat (tb2tn s') s'
destruct s', s; unfold tb2tn, tmap; simpl .d : duration n1 : nat st : seq (duration * nat) IHst : forall st' : seq (binnat.N * binnat.N),
m_tb2tn st' = st ->
list_R (prod_R Rnat Rnat) (m_tb2tn st') st'n, n0 : binnat.N st' : seq (binnat.N * binnat.N) H1 : m_tb2tn ((n, n0) :: st') = (d, n1) :: st H0 : tb2tn (n, n0) = (d, n1) H2 : m_tb2tn st' = st
prod_R Rnat Rnat (n, n0) (n, n0)
by apply refinesP; refines_apply. }
Qed .
(** Next, we prove a refinement for [repeat_steps_with_offset]. *)
Global Instance refine_repeat_steps_with_offset :
refines (Rtask ==> list_R Rnat ==> list_R Rnat)%rel
repeat_steps_with_offset repeat_steps_with_offset_T.refines (Rtask ==> list_R Rnat ==> list_R Rnat)
repeat_steps_with_offset repeat_steps_with_offset_T
Proof .refines (Rtask ==> list_R Rnat ==> list_R Rnat)
repeat_steps_with_offset repeat_steps_with_offset_T
rewrite refinesE => tsk tsk' Rtsk os os' Ros.tsk : Task tsk' : task_T Rtsk : Rtask tsk tsk' os : seq nat os' : seq binnat.N Ros : list_R Rnat os os'
list_R Rnat (repeat_steps_with_offset tsk os)
(repeat_steps_with_offset_T tsk' os')
apply flatten_R; eapply map_R; last by apply Ros.tsk : Task tsk' : task_T Rtsk : Rtask tsk tsk' os : seq nat os' : seq binnat.N Ros : list_R Rnat os os'
forall (t₁ : nat) (t₂ : binnat.N),
Rnat t₁ t₂ ->
list_R Rnat (time_steps_with_offset tsk t₁)
(time_steps_with_offset_T tsk' t₂)
intros o o' Ro.tsk : Task tsk' : task_T Rtsk : Rtask tsk tsk' os : seq nat os' : seq binnat.N Ros : list_R Rnat os os' o : nat o' : binnat.N Ro : Rnat o o'
list_R Rnat (time_steps_with_offset tsk o)
(time_steps_with_offset_T tsk' o')
eapply map_R.tsk : Task tsk' : task_T Rtsk : Rtask tsk tsk' os : seq nat os' : seq binnat.N Ros : list_R Rnat os os' o : nat o' : binnat.N Ro : Rnat o o'
forall (t₁ : nat) (t₂ : binnat.N),
?T1_R t₁ t₂ -> Rnat (t₁ + o) (t₂ + o')%C
{ tsk : Task tsk' : task_T Rtsk : Rtask tsk tsk' os : seq nat os' : seq binnat.N Ros : list_R Rnat os os' o : nat o' : binnat.N Ro : Rnat o o'
forall (t₁ : nat) (t₂ : binnat.N),
?T1_R t₁ t₂ -> Rnat (t₁ + o) (t₂ + o')%C
by intros a a' Ra; apply refinesP; refines_apply. } tsk : Task tsk' : task_T Rtsk : Rtask tsk tsk' os : seq nat os' : seq binnat.N Ros : list_R Rnat os os' o : nat o' : binnat.N Ro : Rnat o o'
list_R Rnat (get_time_steps_of_task tsk)
(get_time_steps_of_task_T tsk')
{ tsk : Task tsk' : task_T Rtsk : Rtask tsk tsk' os : seq nat os' : seq binnat.N Ros : list_R Rnat os os' o : nat o' : binnat.N Ro : Rnat o o'
list_R Rnat (get_time_steps_of_task tsk)
(get_time_steps_of_task_T tsk')
unfold get_time_steps_of_task, get_time_steps_of_task_T.tsk : Task tsk' : task_T Rtsk : Rtask tsk tsk' os : seq nat os' : seq binnat.N Ros : list_R Rnat os os' o : nat o' : binnat.N Ro : Rnat o o'
list_R Rnat
(time_steps_of (get_arrival_curve_prefix tsk))
(time_steps_of_T
(get_extrapolated_arrival_curve_T tsk'))
have Rab := refine_task_arrival.tsk : Task tsk' : task_T Rtsk : Rtask tsk tsk' os : seq nat os' : seq binnat.N Ros : list_R Rnat os os' o : nat o' : binnat.N Ro : Rnat o o' Rab : refines (Rtask ==> Rtask_ab) task_arrival
task_arrival_T
list_R Rnat
(time_steps_of (get_arrival_curve_prefix tsk))
(time_steps_of_T
(get_extrapolated_arrival_curve_T tsk'))
rewrite refinesE in Rab; specialize (Rab _ _ Rtsk).tsk : Task tsk' : task_T Rtsk : Rtask tsk tsk' os : seq nat os' : seq binnat.N Ros : list_R Rnat os os' o : nat o' : binnat.N Ro : Rnat o o' Rab : Rtask_ab (task_arrival tsk)
(task_arrival_T tsk')
list_R Rnat
(time_steps_of (get_arrival_curve_prefix tsk))
(time_steps_of_T
(get_extrapolated_arrival_curve_T tsk'))
rewrite /get_arrival_curve_prefix /get_extrapolated_arrival_curve_T.tsk : Task tsk' : task_T Rtsk : Rtask tsk tsk' os : seq nat os' : seq binnat.N Ros : list_R Rnat os os' o : nat o' : binnat.N Ro : Rnat o o' Rab : Rtask_ab (task_arrival tsk)
(task_arrival_T tsk')
list_R Rnat
(time_steps_of
match task_arrival tsk with
| Periodic p => inter_arrival_to_prefix p
| Sporadic m => inter_arrival_to_prefix m
| ArrivalPrefix steps => steps
end )
(time_steps_of_T
match task_arrival_T tsk' with
| Periodic_T p =>
inter_arrival_to_extrapolated_arrival_curve_T
p
| Sporadic_T m =>
inter_arrival_to_extrapolated_arrival_curve_T
m
| ArrivalPrefix_T steps => steps
end )
destruct (task_arrival tsk) as [?|?|arrival_curve_prefix], (task_arrival_T tsk') as [?|?|arrival_curve_prefixT].tsk : Task tsk' : task_T Rtsk : Rtask tsk tsk' os : seq nat os' : seq binnat.N Ros : list_R Rnat os os' o : nat o' : binnat.N Ro : Rnat o o' n : nat n0 : binnat.N Rab : Rtask_ab (Periodic n) (Periodic_T n0)
list_R Rnat
(time_steps_of (inter_arrival_to_prefix n))
(time_steps_of_T
(inter_arrival_to_extrapolated_arrival_curve_T n0))
all : try (inversion Rab; fail ).tsk : Task tsk' : task_T Rtsk : Rtask tsk tsk' os : seq nat os' : seq binnat.N Ros : list_R Rnat os os' o : nat o' : binnat.N Ro : Rnat o o' n : nat n0 : binnat.N Rab : Rtask_ab (Periodic n) (Periodic_T n0)
list_R Rnat
(time_steps_of (inter_arrival_to_prefix n))
(time_steps_of_T
(inter_arrival_to_extrapolated_arrival_curve_T n0))
all : unfold inter_arrival_to_prefix, inter_arrival_to_extrapolated_arrival_curve_T.tsk : Task tsk' : task_T Rtsk : Rtask tsk tsk' os : seq nat os' : seq binnat.N Ros : list_R Rnat os os' o : nat o' : binnat.N Ro : Rnat o o' n : nat n0 : binnat.N Rab : Rtask_ab (Periodic n) (Periodic_T n0)
list_R Rnat (time_steps_of (n, [:: (1 , 1 )]))
(time_steps_of_T (n0, [:: (1 %C, 1 %C)]))
{ tsk : Task tsk' : task_T Rtsk : Rtask tsk tsk' os : seq nat os' : seq binnat.N Ros : list_R Rnat os os' o : nat o' : binnat.N Ro : Rnat o o' n : nat n0 : binnat.N Rab : Rtask_ab (Periodic n) (Periodic_T n0)
list_R Rnat (time_steps_of (n, [:: (1 , 1 )]))
(time_steps_of_T (n0, [:: (1 %C, 1 %C)]))
apply refinesP; refines_apply.tsk : Task tsk' : task_T Rtsk : Rtask tsk tsk' os : seq nat os' : seq binnat.N Ros : list_R Rnat os os' o : nat o' : binnat.N Ro : Rnat o o' n : nat n0 : binnat.N Rab : Rtask_ab (Periodic n) (Periodic_T n0)
refines Rnat n n0
by rewrite refinesE; inversion Rab; subst . } tsk : Task tsk' : task_T Rtsk : Rtask tsk tsk' os : seq nat os' : seq binnat.N Ros : list_R Rnat os os' o : nat o' : binnat.N Ro : Rnat o o' n : nat n0 : binnat.N Rab : Rtask_ab (Sporadic n) (Sporadic_T n0)
list_R Rnat (time_steps_of (n, [:: (1 , 1 )]))
(time_steps_of_T (n0, [:: (1 %C, 1 %C)]))
{ tsk : Task tsk' : task_T Rtsk : Rtask tsk tsk' os : seq nat os' : seq binnat.N Ros : list_R Rnat os os' o : nat o' : binnat.N Ro : Rnat o o' n : nat n0 : binnat.N Rab : Rtask_ab (Sporadic n) (Sporadic_T n0)
list_R Rnat (time_steps_of (n, [:: (1 , 1 )]))
(time_steps_of_T (n0, [:: (1 %C, 1 %C)]))
apply refinesP; refines_apply.tsk : Task tsk' : task_T Rtsk : Rtask tsk tsk' os : seq nat os' : seq binnat.N Ros : list_R Rnat os os' o : nat o' : binnat.N Ro : Rnat o o' n : nat n0 : binnat.N Rab : Rtask_ab (Sporadic n) (Sporadic_T n0)
refines Rnat n n0
by rewrite refinesE; inversion Rab; subst . } tsk : Task tsk' : task_T Rtsk : Rtask tsk tsk' os : seq nat os' : seq binnat.N Ros : list_R Rnat os os' o : nat o' : binnat.N Ro : Rnat o o' arrival_curve_prefix : ArrivalCurvePrefix arrival_curve_prefixT : (binnat.N *
seq (binnat.N * binnat.N))%type Rab : Rtask_ab (ArrivalPrefix arrival_curve_prefix)
(ArrivalPrefix_T arrival_curve_prefixT)
list_R Rnat (time_steps_of arrival_curve_prefix)
(time_steps_of_T arrival_curve_prefixT)
{ tsk : Task tsk' : task_T Rtsk : Rtask tsk tsk' os : seq nat os' : seq binnat.N Ros : list_R Rnat os os' o : nat o' : binnat.N Ro : Rnat o o' arrival_curve_prefix : ArrivalCurvePrefix arrival_curve_prefixT : (binnat.N *
seq (binnat.N * binnat.N))%type Rab : Rtask_ab (ArrivalPrefix arrival_curve_prefix)
(ArrivalPrefix_T arrival_curve_prefixT)
list_R Rnat (time_steps_of arrival_curve_prefix)
(time_steps_of_T arrival_curve_prefixT)
apply refinesP; refines_apply.tsk : Task tsk' : task_T Rtsk : Rtask tsk tsk' os : seq nat os' : seq binnat.N Ros : list_R Rnat os os' o : nat o' : binnat.N Ro : Rnat o o' arrival_curve_prefix : ArrivalCurvePrefix arrival_curve_prefixT : (binnat.N *
seq (binnat.N * binnat.N))%type Rab : Rtask_ab (ArrivalPrefix arrival_curve_prefix)
(ArrivalPrefix_T arrival_curve_prefixT)
refines (prod_R Rnat (list_R (prod_R Rnat Rnat)))
arrival_curve_prefix arrival_curve_prefixT
destruct arrival_curve_prefix as [h st], arrival_curve_prefixT as [h' st'].tsk : Task tsk' : task_T Rtsk : Rtask tsk tsk' os : seq nat os' : seq binnat.N Ros : list_R Rnat os os' o : nat o' : binnat.N Ro : Rnat o o' h : duration st : seq (duration * nat) h' : binnat.N st' : seq (binnat.N * binnat.N) Rab : Rtask_ab (ArrivalPrefix (h, st))
(ArrivalPrefix_T (h', st'))
refines (prod_R Rnat (list_R (prod_R Rnat Rnat)))
(h, st) (h', st')
inversion Rab as [(H0, H1)]; refines_apply.tsk : Task tsk' : task_T Rtsk : Rtask tsk tsk' os : seq nat os' : seq binnat.N Ros : list_R Rnat os os' o : nat o' : binnat.N Ro : Rnat o o' h : duration st : seq (duration * nat) h' : binnat.N st' : seq (binnat.N * binnat.N) Rab : Rtask_ab (ArrivalPrefix (h, st))
(ArrivalPrefix_T (h', st')) H0 : h' = h H1 : m_tb2tn st' = st
refines (list_R (prod_R Rnat Rnat)) (m_tb2tn st') st'
move : H1; clear ; move : st'.st : seq (duration * nat)
forall st' : seq (binnat.N * binnat.N),
m_tb2tn st' = st ->
refines (list_R (prod_R Rnat Rnat)) (m_tb2tn st') st'
rewrite refinesE; elim : st => [|a st IHst] [ |s st'] //.m_tb2tn [::] = [::] ->
list_R (prod_R Rnat Rnat) (m_tb2tn [::]) [::]
- m_tb2tn [::] = [::] ->
list_R (prod_R Rnat Rnat) (m_tb2tn [::]) [::]
by intros _; rewrite //=; apply list_R_nil_R.
- a : (duration * nat)%type st : seq (duration * nat) IHst : forall st' : seq (binnat.N * binnat.N),
m_tb2tn st' = st ->
list_R (prod_R Rnat Rnat) (m_tb2tn st') st's : (binnat.N * binnat.N)%type st' : seq (binnat.N * binnat.N)
m_tb2tn (s :: st') = a :: st ->
list_R (prod_R Rnat Rnat) (m_tb2tn (s :: st'))
(s :: st')
intros H1; inversion H1; rewrite //=.a : (duration * nat)%type st : seq (duration * nat) IHst : forall st' : seq (binnat.N * binnat.N),
m_tb2tn st' = st ->
list_R (prod_R Rnat Rnat) (m_tb2tn st') st's : (binnat.N * binnat.N)%type st' : seq (binnat.N * binnat.N) H1 : m_tb2tn (s :: st') = a :: st H0 : tb2tn s = a H2 : m_tb2tn st' = st
list_R (prod_R Rnat Rnat) (tb2tn s :: m_tb2tn st')
(s :: st')
apply list_R_cons_R; last by apply IHst.a : (duration * nat)%type st : seq (duration * nat) IHst : forall st' : seq (binnat.N * binnat.N),
m_tb2tn st' = st ->
list_R (prod_R Rnat Rnat) (m_tb2tn st') st's : (binnat.N * binnat.N)%type st' : seq (binnat.N * binnat.N) H1 : m_tb2tn (s :: st') = a :: st H0 : tb2tn s = a H2 : m_tb2tn st' = st
prod_R Rnat Rnat (tb2tn s) s
destruct s, a; unfold tb2tn, tmap; simpl .d : duration n1 : nat st : seq (duration * nat) IHst : forall st' : seq (binnat.N * binnat.N),
m_tb2tn st' = st ->
list_R (prod_R Rnat Rnat) (m_tb2tn st') st'n, n0 : binnat.N st' : seq (binnat.N * binnat.N) H1 : m_tb2tn ((n, n0) :: st') = (d, n1) :: st H0 : tb2tn (n, n0) = (d, n1) H2 : m_tb2tn st' = st
prod_R Rnat Rnat (n, n0) (n, n0)
by apply refinesP; refines_apply. } }
Qed .
(** Next, we prove a refinement for [get_horizon_of_task]. *)
Global Instance refine_get_horizon_of_task :
refines (Rtask ==> Rnat)%rel get_horizon_of_task get_horizon_of_task_T.refines (Rtask ==> Rnat) get_horizon_of_task
get_horizon_of_task_T
Proof .refines (Rtask ==> Rnat) get_horizon_of_task
get_horizon_of_task_T
rewrite refinesE => tsk tsk' Rtsk.tsk : Task tsk' : task_T Rtsk : Rtask tsk tsk'
Rnat (get_horizon_of_task tsk)
(get_horizon_of_task_T tsk')
rewrite /get_horizon_of_task /get_horizon_of_task_T.tsk : Task tsk' : task_T Rtsk : Rtask tsk tsk'
Rnat (horizon_of (get_arrival_curve_prefix tsk))
(horizon_of_T
(get_extrapolated_arrival_curve_T tsk'))
have Rab := refine_task_arrival.tsk : Task tsk' : task_T Rtsk : Rtask tsk tsk' Rab : refines (Rtask ==> Rtask_ab) task_arrival
task_arrival_T
Rnat (horizon_of (get_arrival_curve_prefix tsk))
(horizon_of_T
(get_extrapolated_arrival_curve_T tsk'))
rewrite refinesE in Rab; specialize (Rab _ _ Rtsk).tsk : Task tsk' : task_T Rtsk : Rtask tsk tsk' Rab : Rtask_ab (task_arrival tsk)
(task_arrival_T tsk')
Rnat (horizon_of (get_arrival_curve_prefix tsk))
(horizon_of_T
(get_extrapolated_arrival_curve_T tsk'))
rewrite /get_arrival_curve_prefix /get_extrapolated_arrival_curve_T.tsk : Task tsk' : task_T Rtsk : Rtask tsk tsk' Rab : Rtask_ab (task_arrival tsk)
(task_arrival_T tsk')
Rnat
(horizon_of
match task_arrival tsk with
| Periodic p => inter_arrival_to_prefix p
| Sporadic m => inter_arrival_to_prefix m
| ArrivalPrefix steps => steps
end )
(horizon_of_T
match task_arrival_T tsk' with
| Periodic_T p =>
inter_arrival_to_extrapolated_arrival_curve_T
p
| Sporadic_T m =>
inter_arrival_to_extrapolated_arrival_curve_T
m
| ArrivalPrefix_T steps => steps
end )
destruct (task_arrival _) as [?|?|arrival_curve_prefix], (task_arrival_T _) as [?|?|arrival_curve_prefixT].tsk : Task tsk' : task_T Rtsk : Rtask tsk tsk' n : nat n0 : binnat.N Rab : Rtask_ab (Periodic n) (Periodic_T n0)
Rnat (horizon_of (inter_arrival_to_prefix n))
(horizon_of_T
(inter_arrival_to_extrapolated_arrival_curve_T n0))
all : try (inversion Rab; fail ).tsk : Task tsk' : task_T Rtsk : Rtask tsk tsk' n : nat n0 : binnat.N Rab : Rtask_ab (Periodic n) (Periodic_T n0)
Rnat (horizon_of (inter_arrival_to_prefix n))
(horizon_of_T
(inter_arrival_to_extrapolated_arrival_curve_T n0))
all : unfold inter_arrival_to_prefix, inter_arrival_to_extrapolated_arrival_curve_T.tsk : Task tsk' : task_T Rtsk : Rtask tsk tsk' n : nat n0 : binnat.N Rab : Rtask_ab (Periodic n) (Periodic_T n0)
Rnat (horizon_of (n, [:: (1 , 1 )]))
(horizon_of_T (n0, [:: (1 %C, 1 %C)]))
{ tsk : Task tsk' : task_T Rtsk : Rtask tsk tsk' n : nat n0 : binnat.N Rab : Rtask_ab (Periodic n) (Periodic_T n0)
Rnat (horizon_of (n, [:: (1 , 1 )]))
(horizon_of_T (n0, [:: (1 %C, 1 %C)]))
apply refinesP; refines_apply.tsk : Task tsk' : task_T Rtsk : Rtask tsk tsk' n : nat n0 : binnat.N Rab : Rtask_ab (Periodic n) (Periodic_T n0)
refines Rnat n n0
by rewrite refinesE; inversion Rab; subst . } tsk : Task tsk' : task_T Rtsk : Rtask tsk tsk' n : nat n0 : binnat.N Rab : Rtask_ab (Sporadic n) (Sporadic_T n0)
Rnat (horizon_of (n, [:: (1 , 1 )]))
(horizon_of_T (n0, [:: (1 %C, 1 %C)]))
{ tsk : Task tsk' : task_T Rtsk : Rtask tsk tsk' n : nat n0 : binnat.N Rab : Rtask_ab (Sporadic n) (Sporadic_T n0)
Rnat (horizon_of (n, [:: (1 , 1 )]))
(horizon_of_T (n0, [:: (1 %C, 1 %C)]))
apply refinesP; refines_apply.tsk : Task tsk' : task_T Rtsk : Rtask tsk tsk' n : nat n0 : binnat.N Rab : Rtask_ab (Sporadic n) (Sporadic_T n0)
refines Rnat n n0
by rewrite refinesE; inversion Rab; subst . } tsk : Task tsk' : task_T Rtsk : Rtask tsk tsk' arrival_curve_prefix : ArrivalCurvePrefix arrival_curve_prefixT : (binnat.N *
seq (binnat.N * binnat.N))%type Rab : Rtask_ab (ArrivalPrefix arrival_curve_prefix)
(ArrivalPrefix_T arrival_curve_prefixT)
Rnat (horizon_of arrival_curve_prefix)
(horizon_of_T arrival_curve_prefixT)
{ tsk : Task tsk' : task_T Rtsk : Rtask tsk tsk' arrival_curve_prefix : ArrivalCurvePrefix arrival_curve_prefixT : (binnat.N *
seq (binnat.N * binnat.N))%type Rab : Rtask_ab (ArrivalPrefix arrival_curve_prefix)
(ArrivalPrefix_T arrival_curve_prefixT)
Rnat (horizon_of arrival_curve_prefix)
(horizon_of_T arrival_curve_prefixT)
destruct arrival_curve_prefix as [h st], arrival_curve_prefixT as [h' st'].tsk : Task tsk' : task_T Rtsk : Rtask tsk tsk' h : duration st : seq (duration * nat) h' : binnat.N st' : seq (binnat.N * binnat.N) Rab : Rtask_ab (ArrivalPrefix (h, st))
(ArrivalPrefix_T (h', st'))
Rnat (horizon_of (h, st)) (horizon_of_T (h', st'))
rewrite /horizon_of /horizon_of_T //=.tsk : Task tsk' : task_T Rtsk : Rtask tsk tsk' h : duration st : seq (duration * nat) h' : binnat.N st' : seq (binnat.N * binnat.N) Rab : Rtask_ab (ArrivalPrefix (h, st))
(ArrivalPrefix_T (h', st'))
Rnat h h'
by inversion Rab; apply refinesP; tc. }
Qed .
(** Next, we prove a refinement for the extrapolated arrival curve. *)
Local Instance refine_extrapolated_arrival_curve :
forall arrival_curve_prefix arrival_curve_prefixT δ δ' ,
refines Rnat δ δ' ->
Rtask_ab (ArrivalPrefix arrival_curve_prefix) (ArrivalPrefix_T arrival_curve_prefixT) ->
refines Rnat (extrapolated_arrival_curve arrival_curve_prefix δ) (extrapolated_arrival_curve_T arrival_curve_prefixT δ').forall (arrival_curve_prefix : ArrivalCurvePrefix)
(arrival_curve_prefixT : binnat.N *
seq (binnat.N * binnat.N))
(δ : nat) (δ' : binnat.N),
refines Rnat δ δ' ->
Rtask_ab (ArrivalPrefix arrival_curve_prefix)
(ArrivalPrefix_T arrival_curve_prefixT) ->
refines Rnat
(extrapolated_arrival_curve arrival_curve_prefix δ)
(extrapolated_arrival_curve_T arrival_curve_prefixT
δ')
Proof .forall (arrival_curve_prefix : ArrivalCurvePrefix)
(arrival_curve_prefixT : binnat.N *
seq (binnat.N * binnat.N))
(δ : nat) (δ' : binnat.N),
refines Rnat δ δ' ->
Rtask_ab (ArrivalPrefix arrival_curve_prefix)
(ArrivalPrefix_T arrival_curve_prefixT) ->
refines Rnat
(extrapolated_arrival_curve arrival_curve_prefix δ)
(extrapolated_arrival_curve_T arrival_curve_prefixT
δ')
move => arrival_curve_prefix arrival_curve_prefixT δ δ' Rδ Rab.arrival_curve_prefix : ArrivalCurvePrefix arrival_curve_prefixT : (binnat.N *
seq (binnat.N * binnat.N))%type δ : nat δ' : binnat.N Rδ : refines Rnat δ δ' Rab : Rtask_ab (ArrivalPrefix arrival_curve_prefix)
(ArrivalPrefix_T arrival_curve_prefixT)
refines Rnat
(extrapolated_arrival_curve arrival_curve_prefix δ)
(extrapolated_arrival_curve_T arrival_curve_prefixT
δ')
refines_apply. arrival_curve_prefix : ArrivalCurvePrefix arrival_curve_prefixT : (binnat.N *
seq (binnat.N * binnat.N))%type δ : nat δ' : binnat.N Rδ : refines Rnat δ δ' Rab : Rtask_ab (ArrivalPrefix arrival_curve_prefix)
(ArrivalPrefix_T arrival_curve_prefixT)
refines (prod_R Rnat (list_R (prod_R Rnat Rnat)))
arrival_curve_prefix arrival_curve_prefixT
destruct arrival_curve_prefix as [h st], arrival_curve_prefixT as [h' st'].h : duration st : seq (duration * nat) h' : binnat.N st' : seq (binnat.N * binnat.N) δ : nat δ' : binnat.N Rδ : refines Rnat δ δ' Rab : Rtask_ab (ArrivalPrefix (h, st)) (ArrivalPrefix_T (h', st'))
refines (prod_R Rnat (list_R (prod_R Rnat Rnat)))
(h, st) (h', st')
inversion Rab as [(H0, H1)]; refines_apply.h : duration st : seq (duration * nat) h' : binnat.N st' : seq (binnat.N * binnat.N) δ : nat δ' : binnat.N Rδ : refines Rnat δ δ' Rab : Rtask_ab (ArrivalPrefix (h, st)) (ArrivalPrefix_T (h', st')) H0 : h' = h H1 : m_tb2tn st' = st
refines (list_R (prod_R Rnat Rnat)) (m_tb2tn st') st'
move : H1; clear ; move : st'.st : seq (duration * nat)
forall st' : seq (binnat.N * binnat.N),
m_tb2tn st' = st ->
refines (list_R (prod_R Rnat Rnat)) (m_tb2tn st') st'
rewrite refinesE; elim : st => [|a st IHst] [ |s st'] //.m_tb2tn [::] = [::] ->
list_R (prod_R Rnat Rnat) (m_tb2tn [::]) [::]
- m_tb2tn [::] = [::] ->
list_R (prod_R Rnat Rnat) (m_tb2tn [::]) [::]
by intros _; rewrite //=; apply list_R_nil_R.
- a : (duration * nat)%type st : seq (duration * nat) IHst : forall st' : seq (binnat.N * binnat.N),
m_tb2tn st' = st ->
list_R (prod_R Rnat Rnat) (m_tb2tn st') st's : (binnat.N * binnat.N)%type st' : seq (binnat.N * binnat.N)
m_tb2tn (s :: st') = a :: st ->
list_R (prod_R Rnat Rnat) (m_tb2tn (s :: st'))
(s :: st')
intros H1; inversion H1; rewrite //=.a : (duration * nat)%type st : seq (duration * nat) IHst : forall st' : seq (binnat.N * binnat.N),
m_tb2tn st' = st ->
list_R (prod_R Rnat Rnat) (m_tb2tn st') st's : (binnat.N * binnat.N)%type st' : seq (binnat.N * binnat.N) H1 : m_tb2tn (s :: st') = a :: st H0 : tb2tn s = a H2 : m_tb2tn st' = st
list_R (prod_R Rnat Rnat) (tb2tn s :: m_tb2tn st')
(s :: st')
apply list_R_cons_R; last by apply IHst.a : (duration * nat)%type st : seq (duration * nat) IHst : forall st' : seq (binnat.N * binnat.N),
m_tb2tn st' = st ->
list_R (prod_R Rnat Rnat) (m_tb2tn st') st's : (binnat.N * binnat.N)%type st' : seq (binnat.N * binnat.N) H1 : m_tb2tn (s :: st') = a :: st H0 : tb2tn s = a H2 : m_tb2tn st' = st
prod_R Rnat Rnat (tb2tn s) s
destruct s, a; unfold tb2tn, tmap; simpl .d : duration n1 : nat st : seq (duration * nat) IHst : forall st' : seq (binnat.N * binnat.N),
m_tb2tn st' = st ->
list_R (prod_R Rnat Rnat) (m_tb2tn st') st'n, n0 : binnat.N st' : seq (binnat.N * binnat.N) H1 : m_tb2tn ((n, n0) :: st') = (d, n1) :: st H0 : tb2tn (n, n0) = (d, n1) H2 : m_tb2tn st' = st
prod_R Rnat Rnat (n, n0) (n, n0)
by apply refinesP; refines_apply.
Qed .
(** Next, we prove a refinement for the arrival bound definition. *)
Local Instance refine_ConcreteMaxArrivals :
refines ( Rtask ==> Rnat ==> Rnat )%rel ConcreteMaxArrivals ConcreteMaxArrivals_T.refines (Rtask ==> Rnat ==> Rnat) ConcreteMaxArrivals
ConcreteMaxArrivals_T
Proof .refines (Rtask ==> Rnat ==> Rnat) ConcreteMaxArrivals
ConcreteMaxArrivals_T
apply refines_abstr2.forall (a : Task) (b : task_T),
refines Rtask a b ->
forall (a' : nat) (b' : binnat.N),
refines Rnat a' b' ->
refines Rnat (ConcreteMaxArrivals a a')
(ConcreteMaxArrivals_T b b')
rewrite /ConcreteMaxArrivals /concrete_max_arrivals /ConcreteMaxArrivals_T.forall (a : Task) (b : task_T),
refines Rtask a b ->
forall (a' : nat) (b' : binnat.N),
refines Rnat a' b' ->
refines Rnat
(extrapolated_arrival_curve
(get_arrival_curve_prefix a) a')
(extrapolated_arrival_curve_T
(get_extrapolated_arrival_curve_T b) b')
move => tsk tsk' Rtsk δ δ' Rδ.tsk : Task tsk' : task_T Rtsk : refines Rtask tsk tsk' δ : nat δ' : binnat.N Rδ : refines Rnat δ δ'
refines Rnat
(extrapolated_arrival_curve
(get_arrival_curve_prefix tsk) δ)
(extrapolated_arrival_curve_T
(get_extrapolated_arrival_curve_T tsk') δ')
have Rab := refine_task_arrival.tsk : Task tsk' : task_T Rtsk : refines Rtask tsk tsk' δ : nat δ' : binnat.N Rδ : refines Rnat δ δ' Rab : refines (Rtask ==> Rtask_ab) task_arrival
task_arrival_T
refines Rnat
(extrapolated_arrival_curve
(get_arrival_curve_prefix tsk) δ)
(extrapolated_arrival_curve_T
(get_extrapolated_arrival_curve_T tsk') δ')
rewrite refinesE in Rab; rewrite refinesE in Rtsk.tsk : Task tsk' : task_T δ : nat δ' : binnat.N Rδ : refines Rnat δ δ' Rab : (Rtask ==> Rtask_ab)%rel task_arrival
task_arrival_T Rtsk : Rtask tsk tsk'
refines Rnat
(extrapolated_arrival_curve
(get_arrival_curve_prefix tsk) δ)
(extrapolated_arrival_curve_T
(get_extrapolated_arrival_curve_T tsk') δ')
specialize (Rab _ _ Rtsk).tsk : Task tsk' : task_T δ : nat δ' : binnat.N Rδ : refines Rnat δ δ' Rab : Rtask_ab (task_arrival tsk)
(task_arrival_T tsk') Rtsk : Rtask tsk tsk'
refines Rnat
(extrapolated_arrival_curve
(get_arrival_curve_prefix tsk) δ)
(extrapolated_arrival_curve_T
(get_extrapolated_arrival_curve_T tsk') δ')
rewrite /get_arrival_curve_prefix /get_extrapolated_arrival_curve_T.tsk : Task tsk' : task_T δ : nat δ' : binnat.N Rδ : refines Rnat δ δ' Rab : Rtask_ab (task_arrival tsk)
(task_arrival_T tsk') Rtsk : Rtask tsk tsk'
refines Rnat
(extrapolated_arrival_curve
match task_arrival tsk with
| Periodic p => inter_arrival_to_prefix p
| Sporadic m => inter_arrival_to_prefix m
| ArrivalPrefix steps => steps
end δ)
(extrapolated_arrival_curve_T
match task_arrival_T tsk' with
| Periodic_T p =>
inter_arrival_to_extrapolated_arrival_curve_T
p
| Sporadic_T m =>
inter_arrival_to_extrapolated_arrival_curve_T
m
| ArrivalPrefix_T steps => steps
end δ')
destruct (task_arrival tsk) as [?|?|arrival_curve_prefix], (task_arrival_T tsk') as [?|?|arrival_curve_prefixT].tsk : Task tsk' : task_T δ : nat δ' : binnat.N Rδ : refines Rnat δ δ' n : nat n0 : binnat.N Rab : Rtask_ab (Periodic n) (Periodic_T n0) Rtsk : Rtask tsk tsk'
refines Rnat
(extrapolated_arrival_curve
(inter_arrival_to_prefix n) δ)
(extrapolated_arrival_curve_T
(inter_arrival_to_extrapolated_arrival_curve_T n0)
δ')
all : try (inversion Rab; fail ).tsk : Task tsk' : task_T δ : nat δ' : binnat.N Rδ : refines Rnat δ δ' n : nat n0 : binnat.N Rab : Rtask_ab (Periodic n) (Periodic_T n0) Rtsk : Rtask tsk tsk'
refines Rnat
(extrapolated_arrival_curve
(inter_arrival_to_prefix n) δ)
(extrapolated_arrival_curve_T
(inter_arrival_to_extrapolated_arrival_curve_T n0)
δ')
all : unfold inter_arrival_to_prefix, inter_arrival_to_extrapolated_arrival_curve_T.tsk : Task tsk' : task_T δ : nat δ' : binnat.N Rδ : refines Rnat δ δ' n : nat n0 : binnat.N Rab : Rtask_ab (Periodic n) (Periodic_T n0) Rtsk : Rtask tsk tsk'
refines Rnat
(extrapolated_arrival_curve (n, [:: (1 , 1 )]) δ)
(extrapolated_arrival_curve_T (n0, [:: (1 %C, 1 %C)])
δ')
{ tsk : Task tsk' : task_T δ : nat δ' : binnat.N Rδ : refines Rnat δ δ' n : nat n0 : binnat.N Rab : Rtask_ab (Periodic n) (Periodic_T n0) Rtsk : Rtask tsk tsk'
refines Rnat
(extrapolated_arrival_curve (n, [:: (1 , 1 )]) δ)
(extrapolated_arrival_curve_T (n0, [:: (1 %C, 1 %C)])
δ')
by refines_apply; rewrite refinesE; inversion Rab; subst . } tsk : Task tsk' : task_T δ : nat δ' : binnat.N Rδ : refines Rnat δ δ' n : nat n0 : binnat.N Rab : Rtask_ab (Sporadic n) (Sporadic_T n0) Rtsk : Rtask tsk tsk'
refines Rnat
(extrapolated_arrival_curve (n, [:: (1 , 1 )]) δ)
(extrapolated_arrival_curve_T (n0, [:: (1 %C, 1 %C)])
δ')
{ tsk : Task tsk' : task_T δ : nat δ' : binnat.N Rδ : refines Rnat δ δ' n : nat n0 : binnat.N Rab : Rtask_ab (Sporadic n) (Sporadic_T n0) Rtsk : Rtask tsk tsk'
refines Rnat
(extrapolated_arrival_curve (n, [:: (1 , 1 )]) δ)
(extrapolated_arrival_curve_T (n0, [:: (1 %C, 1 %C)])
δ')
by refines_apply; rewrite refinesE; inversion Rab; subst . } tsk : Task tsk' : task_T δ : nat δ' : binnat.N Rδ : refines Rnat δ δ' arrival_curve_prefix : ArrivalCurvePrefix arrival_curve_prefixT : (binnat.N *
seq (binnat.N * binnat.N))%type Rab : Rtask_ab (ArrivalPrefix arrival_curve_prefix)
(ArrivalPrefix_T arrival_curve_prefixT) Rtsk : Rtask tsk tsk'
refines Rnat
(extrapolated_arrival_curve arrival_curve_prefix δ)
(extrapolated_arrival_curve_T arrival_curve_prefixT
δ')
{ tsk : Task tsk' : task_T δ : nat δ' : binnat.N Rδ : refines Rnat δ δ' arrival_curve_prefix : ArrivalCurvePrefix arrival_curve_prefixT : (binnat.N *
seq (binnat.N * binnat.N))%type Rab : Rtask_ab (ArrivalPrefix arrival_curve_prefix)
(ArrivalPrefix_T arrival_curve_prefixT) Rtsk : Rtask tsk tsk'
refines Rnat
(extrapolated_arrival_curve arrival_curve_prefix δ)
(extrapolated_arrival_curve_T arrival_curve_prefixT
δ')
by apply refine_extrapolated_arrival_curve. }
Qed .
(** Next, we prove a refinement for the arrival bound definition applied to the
task conversion function. *)
Global Instance refine_ConcreteMaxArrivals' :
forall tsk ,
refines (Rnat ==> Rnat)%rel (ConcreteMaxArrivals (taskT_to_task tsk))
(ConcreteMaxArrivals_T tsk) | 0 .forall tsk : task_T,
refines (Rnat ==> Rnat)
(ConcreteMaxArrivals (taskT_to_task tsk))
(ConcreteMaxArrivals_T tsk)
Proof .forall tsk : task_T,
refines (Rnat ==> Rnat)
(ConcreteMaxArrivals (taskT_to_task tsk))
(ConcreteMaxArrivals_T tsk)
intros tsk; apply refines_abstr.tsk : task_T
forall (a : nat) (b : binnat.N),
refines Rnat a b ->
refines Rnat
(ConcreteMaxArrivals (taskT_to_task tsk) a)
(ConcreteMaxArrivals_T tsk b)
rewrite /ConcreteMaxArrivals /concrete_max_arrivals
/ConcreteMaxArrivals_T => δ δ' Rδ.tsk : task_T δ : nat δ' : binnat.N Rδ : refines Rnat δ δ'
refines Rnat
(extrapolated_arrival_curve
(get_arrival_curve_prefix (taskT_to_task tsk)) δ)
(extrapolated_arrival_curve_T
(get_extrapolated_arrival_curve_T tsk) δ')
have Rtsk := refine_task'.tsk : task_T δ : nat δ' : binnat.N Rδ : refines Rnat δ δ' Rtsk : refines (unify (A:=task_T) ==> Rtask)
taskT_to_task id
refines Rnat
(extrapolated_arrival_curve
(get_arrival_curve_prefix (taskT_to_task tsk)) δ)
(extrapolated_arrival_curve_T
(get_extrapolated_arrival_curve_T tsk) δ')
rewrite refinesE in Rtsk.tsk : task_T δ : nat δ' : binnat.N Rδ : refines Rnat δ δ' Rtsk : (unify (A:=task_T) ==> Rtask)%rel taskT_to_task
id
refines Rnat
(extrapolated_arrival_curve
(get_arrival_curve_prefix (taskT_to_task tsk)) δ)
(extrapolated_arrival_curve_T
(get_extrapolated_arrival_curve_T tsk) δ')
specialize (Rtsk tsk tsk (unifyxx _)); simpl in Rtsk.tsk : task_T δ : nat δ' : binnat.N Rδ : refines Rnat δ δ' Rtsk : Rtask (taskT_to_task tsk) tsk
refines Rnat
(extrapolated_arrival_curve
(get_arrival_curve_prefix (taskT_to_task tsk)) δ)
(extrapolated_arrival_curve_T
(get_extrapolated_arrival_curve_T tsk) δ')
have Rab := refine_task_arrival.tsk : task_T δ : nat δ' : binnat.N Rδ : refines Rnat δ δ' Rtsk : Rtask (taskT_to_task tsk) tsk Rab : refines (Rtask ==> Rtask_ab) task_arrival
task_arrival_T
refines Rnat
(extrapolated_arrival_curve
(get_arrival_curve_prefix (taskT_to_task tsk)) δ)
(extrapolated_arrival_curve_T
(get_extrapolated_arrival_curve_T tsk) δ')
rewrite refinesE in Rab.tsk : task_T δ : nat δ' : binnat.N Rδ : refines Rnat δ δ' Rtsk : Rtask (taskT_to_task tsk) tsk Rab : (Rtask ==> Rtask_ab)%rel task_arrival
task_arrival_T
refines Rnat
(extrapolated_arrival_curve
(get_arrival_curve_prefix (taskT_to_task tsk)) δ)
(extrapolated_arrival_curve_T
(get_extrapolated_arrival_curve_T tsk) δ')
specialize (Rab _ _ Rtsk).tsk : task_T δ : nat δ' : binnat.N Rδ : refines Rnat δ δ' Rtsk : Rtask (taskT_to_task tsk) tsk Rab : Rtask_ab (task_arrival (taskT_to_task tsk))
(task_arrival_T tsk)
refines Rnat
(extrapolated_arrival_curve
(get_arrival_curve_prefix (taskT_to_task tsk)) δ)
(extrapolated_arrival_curve_T
(get_extrapolated_arrival_curve_T tsk) δ')
rewrite /get_arrival_curve_prefix /get_extrapolated_arrival_curve_T.tsk : task_T δ : nat δ' : binnat.N Rδ : refines Rnat δ δ' Rtsk : Rtask (taskT_to_task tsk) tsk Rab : Rtask_ab (task_arrival (taskT_to_task tsk))
(task_arrival_T tsk)
refines Rnat
(extrapolated_arrival_curve
match task_arrival (taskT_to_task tsk) with
| Periodic p => inter_arrival_to_prefix p
| Sporadic m => inter_arrival_to_prefix m
| ArrivalPrefix steps => steps
end δ)
(extrapolated_arrival_curve_T
match task_arrival_T tsk with
| Periodic_T p =>
inter_arrival_to_extrapolated_arrival_curve_T
p
| Sporadic_T m =>
inter_arrival_to_extrapolated_arrival_curve_T
m
| ArrivalPrefix_T steps => steps
end δ')
destruct (task_arrival (_ _)) as [?|?|arrival_curve_prefix], (task_arrival_T tsk) as [?|?|arrival_curve_prefixT].tsk : task_T δ : nat δ' : binnat.N Rδ : refines Rnat δ δ' Rtsk : Rtask (taskT_to_task tsk) tsk n : nat n0 : binnat.N Rab : Rtask_ab (Periodic n) (Periodic_T n0)
refines Rnat
(extrapolated_arrival_curve
(inter_arrival_to_prefix n) δ)
(extrapolated_arrival_curve_T
(inter_arrival_to_extrapolated_arrival_curve_T n0)
δ')
all : try (inversion Rab; fail ).tsk : task_T δ : nat δ' : binnat.N Rδ : refines Rnat δ δ' Rtsk : Rtask (taskT_to_task tsk) tsk n : nat n0 : binnat.N Rab : Rtask_ab (Periodic n) (Periodic_T n0)
refines Rnat
(extrapolated_arrival_curve
(inter_arrival_to_prefix n) δ)
(extrapolated_arrival_curve_T
(inter_arrival_to_extrapolated_arrival_curve_T n0)
δ')
all : unfold inter_arrival_to_prefix, inter_arrival_to_extrapolated_arrival_curve_T.tsk : task_T δ : nat δ' : binnat.N Rδ : refines Rnat δ δ' Rtsk : Rtask (taskT_to_task tsk) tsk n : nat n0 : binnat.N Rab : Rtask_ab (Periodic n) (Periodic_T n0)
refines Rnat
(extrapolated_arrival_curve (n, [:: (1 , 1 )]) δ)
(extrapolated_arrival_curve_T (n0, [:: (1 %C, 1 %C)])
δ')
{ tsk : task_T δ : nat δ' : binnat.N Rδ : refines Rnat δ δ' Rtsk : Rtask (taskT_to_task tsk) tsk n : nat n0 : binnat.N Rab : Rtask_ab (Periodic n) (Periodic_T n0)
refines Rnat
(extrapolated_arrival_curve (n, [:: (1 , 1 )]) δ)
(extrapolated_arrival_curve_T (n0, [:: (1 %C, 1 %C)])
δ')
by refines_apply; rewrite refinesE; inversion Rab; subst . } tsk : task_T δ : nat δ' : binnat.N Rδ : refines Rnat δ δ' Rtsk : Rtask (taskT_to_task tsk) tsk n : nat n0 : binnat.N Rab : Rtask_ab (Sporadic n) (Sporadic_T n0)
refines Rnat
(extrapolated_arrival_curve (n, [:: (1 , 1 )]) δ)
(extrapolated_arrival_curve_T (n0, [:: (1 %C, 1 %C)])
δ')
{ tsk : task_T δ : nat δ' : binnat.N Rδ : refines Rnat δ δ' Rtsk : Rtask (taskT_to_task tsk) tsk n : nat n0 : binnat.N Rab : Rtask_ab (Sporadic n) (Sporadic_T n0)
refines Rnat
(extrapolated_arrival_curve (n, [:: (1 , 1 )]) δ)
(extrapolated_arrival_curve_T (n0, [:: (1 %C, 1 %C)])
δ')
by refines_apply; rewrite refinesE; inversion Rab; subst . } tsk : task_T δ : nat δ' : binnat.N Rδ : refines Rnat δ δ' Rtsk : Rtask (taskT_to_task tsk) tsk arrival_curve_prefix : ArrivalCurvePrefix arrival_curve_prefixT : (binnat.N *
seq (binnat.N * binnat.N))%type Rab : Rtask_ab (ArrivalPrefix arrival_curve_prefix)
(ArrivalPrefix_T arrival_curve_prefixT)
refines Rnat
(extrapolated_arrival_curve arrival_curve_prefix δ)
(extrapolated_arrival_curve_T arrival_curve_prefixT
δ')
{ tsk : task_T δ : nat δ' : binnat.N Rδ : refines Rnat δ δ' Rtsk : Rtask (taskT_to_task tsk) tsk arrival_curve_prefix : ArrivalCurvePrefix arrival_curve_prefixT : (binnat.N *
seq (binnat.N * binnat.N))%type Rab : Rtask_ab (ArrivalPrefix arrival_curve_prefix)
(ArrivalPrefix_T arrival_curve_prefixT)
refines Rnat
(extrapolated_arrival_curve arrival_curve_prefix δ)
(extrapolated_arrival_curve_T arrival_curve_prefixT
δ')
by apply refine_extrapolated_arrival_curve. }
Qed .
(** Next, we prove a refinement for [get_arrival_curve_prefix]. *)
Global Instance refine_get_arrival_curve_prefix :
refines (Rtask ==> prod_R Rnat (list_R (prod_R Rnat Rnat)))%rel
get_arrival_curve_prefix get_extrapolated_arrival_curve_T.refines
(Rtask ==> prod_R Rnat (list_R (prod_R Rnat Rnat)))
get_arrival_curve_prefix
get_extrapolated_arrival_curve_T
Proof .refines
(Rtask ==> prod_R Rnat (list_R (prod_R Rnat Rnat)))
get_arrival_curve_prefix
get_extrapolated_arrival_curve_T
rewrite refinesE => tsk tsk' Rtsk.tsk : Task tsk' : task_T Rtsk : Rtask tsk tsk'
prod_R Rnat (list_R (prod_R Rnat Rnat))
(get_arrival_curve_prefix tsk)
(get_extrapolated_arrival_curve_T tsk')
have Rab := refine_task_arrival.tsk : Task tsk' : task_T Rtsk : Rtask tsk tsk' Rab : refines (Rtask ==> Rtask_ab) task_arrival
task_arrival_T
prod_R Rnat (list_R (prod_R Rnat Rnat))
(get_arrival_curve_prefix tsk)
(get_extrapolated_arrival_curve_T tsk')
rewrite refinesE in Rab; specialize (Rab _ _ Rtsk).tsk : Task tsk' : task_T Rtsk : Rtask tsk tsk' Rab : Rtask_ab (task_arrival tsk)
(task_arrival_T tsk')
prod_R Rnat (list_R (prod_R Rnat Rnat))
(get_arrival_curve_prefix tsk)
(get_extrapolated_arrival_curve_T tsk')
rewrite /get_arrival_curve_prefix /get_extrapolated_arrival_curve_T.tsk : Task tsk' : task_T Rtsk : Rtask tsk tsk' Rab : Rtask_ab (task_arrival tsk)
(task_arrival_T tsk')
prod_R Rnat (list_R (prod_R Rnat Rnat))
match task_arrival tsk with
| Periodic p => inter_arrival_to_prefix p
| Sporadic m => inter_arrival_to_prefix m
| ArrivalPrefix steps => steps
end
match task_arrival_T tsk' with
| Periodic_T p =>
inter_arrival_to_extrapolated_arrival_curve_T p
| Sporadic_T m =>
inter_arrival_to_extrapolated_arrival_curve_T m
| ArrivalPrefix_T steps => steps
end
unfold inter_arrival_to_prefix, inter_arrival_to_extrapolated_arrival_curve_T.tsk : Task tsk' : task_T Rtsk : Rtask tsk tsk' Rab : Rtask_ab (task_arrival tsk)
(task_arrival_T tsk')
prod_R Rnat (list_R (prod_R Rnat Rnat))
match task_arrival tsk with
| Periodic p => (p, [:: (1 , 1 )])
| Sporadic m => (m, [:: (1 , 1 )])
| ArrivalPrefix steps => steps
end
match task_arrival_T tsk' with
| Periodic_T p => (p, [:: (1 %C, 1 %C)])
| Sporadic_T m => (m, [:: (1 %C, 1 %C)])
| ArrivalPrefix_T steps => steps
end
destruct (task_arrival _) as [?|?|e], (task_arrival_T _) as [?|?|eT].tsk : Task tsk' : task_T Rtsk : Rtask tsk tsk' n : nat n0 : binnat.N Rab : Rtask_ab (Periodic n) (Periodic_T n0)
prod_R Rnat (list_R (prod_R Rnat Rnat))
(n, [:: (1 , 1 )]) (n0, [:: (1 %C, 1 %C)])
all : try (inversion Rab; fail ).tsk : Task tsk' : task_T Rtsk : Rtask tsk tsk' n : nat n0 : binnat.N Rab : Rtask_ab (Periodic n) (Periodic_T n0)
prod_R Rnat (list_R (prod_R Rnat Rnat))
(n, [:: (1 , 1 )]) (n0, [:: (1 %C, 1 %C)])
all : try (inversion Rab; subst ; apply refinesP; refines_apply; fail ).tsk : Task tsk' : task_T Rtsk : Rtask tsk tsk' e : ArrivalCurvePrefix eT : (binnat.N * seq (binnat.N * binnat.N))%type Rab : Rtask_ab (ArrivalPrefix e) (ArrivalPrefix_T eT)
prod_R Rnat (list_R (prod_R Rnat Rnat)) e eT
destruct e as [h?], eT as [? st];[apply refinesP; refines_apply; inversion Rab; tc].tsk : Task tsk' : task_T Rtsk : Rtask tsk tsk' h : duration l : seq (duration * nat) n : binnat.N st : seq (binnat.N * binnat.N) Rab : Rtask_ab (ArrivalPrefix (h, l))
(ArrivalPrefix_T (n, st)) H0 : n = h H1 : m_tb2tn st = l
refines (list_R (prod_R Rnat Rnat)) (m_tb2tn st) st
inversion Rab as [(H__, Hst)]; subst .tsk : Task tsk' : task_T Rtsk : Rtask tsk tsk' n : binnat.N st : seq (binnat.N * binnat.N) Rab : Rtask_ab (ArrivalPrefix (n, m_tb2tn st))
(ArrivalPrefix_T (n, st)) H__ : n = n Hst : m_tb2tn st = m_tb2tn st
refines (list_R (prod_R Rnat Rnat)) (m_tb2tn st) st
elim : st Rab Hst => [|a st IHst] Rab H1; first by rewrite //= refinesE; apply list_R_nil_R.tsk : Task tsk' : task_T Rtsk : Rtask tsk tsk' n : binnat.N H__ : n = n a : (binnat.N * binnat.N)%type st : seq (binnat.N * binnat.N) IHst : Rtask_ab (ArrivalPrefix (n, m_tb2tn st))
(ArrivalPrefix_T (n, st)) ->
m_tb2tn st = m_tb2tn st ->
refines (list_R (prod_R Rnat Rnat))
(m_tb2tn st) st Rab : Rtask_ab (ArrivalPrefix (n, m_tb2tn (a :: st)))
(ArrivalPrefix_T (n, a :: st)) H1 : m_tb2tn (a :: st) = m_tb2tn (a :: st)
refines (list_R (prod_R Rnat Rnat))
(m_tb2tn (a :: st)) (a :: st)
destruct a; rewrite refinesE.tsk : Task tsk' : task_T Rtsk : Rtask tsk tsk' n : binnat.N H__ : n = n n0, n1 : binnat.N st : seq (binnat.N * binnat.N) IHst : Rtask_ab (ArrivalPrefix (n, m_tb2tn st))
(ArrivalPrefix_T (n, st)) ->
m_tb2tn st = m_tb2tn st ->
refines (list_R (prod_R Rnat Rnat))
(m_tb2tn st) st Rab : Rtask_ab
(ArrivalPrefix (n, m_tb2tn ((n0, n1) :: st)))
(ArrivalPrefix_T (n, (n0, n1) :: st)) H1 : m_tb2tn ((n0, n1) :: st) =
m_tb2tn ((n0, n1) :: st)
list_R (prod_R Rnat Rnat) (m_tb2tn ((n0, n1) :: st))
((n0, n1) :: st)
apply list_R_cons_R; first by apply refinesP; unfold tb2tn,tmap; refines_apply.tsk : Task tsk' : task_T Rtsk : Rtask tsk tsk' n : binnat.N H__ : n = n n0, n1 : binnat.N st : seq (binnat.N * binnat.N) IHst : Rtask_ab (ArrivalPrefix (n, m_tb2tn st))
(ArrivalPrefix_T (n, st)) ->
m_tb2tn st = m_tb2tn st ->
refines (list_R (prod_R Rnat Rnat))
(m_tb2tn st) st Rab : Rtask_ab
(ArrivalPrefix (n, m_tb2tn ((n0, n1) :: st)))
(ArrivalPrefix_T (n, (n0, n1) :: st)) H1 : m_tb2tn ((n0, n1) :: st) =
m_tb2tn ((n0, n1) :: st)
list_R (prod_R Rnat Rnat)
((fix map (s : seq (binnat.N * binnat.N)) :
seq (nat * nat) :=
match s with
| [::] => [::]
| x :: s' => tb2tn x :: map s'
end ) st) st
by apply refinesP, IHst.
Qed .
(** Next, we prove a refinement for [get_arrival_curve_prefix] applied to lists. *)
Global Instance refine_get_arrival_curve_prefix' :
forall tsk ,
refines
(prod_R Rnat (list_R (prod_R Rnat Rnat)))%rel
(get_arrival_curve_prefix (taskT_to_task tsk))
(get_extrapolated_arrival_curve_T tsk) | 0 .forall tsk : task_T,
refines (prod_R Rnat (list_R (prod_R Rnat Rnat)))
(get_arrival_curve_prefix (taskT_to_task tsk))
(get_extrapolated_arrival_curve_T tsk)
Proof .forall tsk : task_T,
refines (prod_R Rnat (list_R (prod_R Rnat Rnat)))
(get_arrival_curve_prefix (taskT_to_task tsk))
(get_extrapolated_arrival_curve_T tsk)
intros tsk.tsk : task_T
refines (prod_R Rnat (list_R (prod_R Rnat Rnat)))
(get_arrival_curve_prefix (taskT_to_task tsk))
(get_extrapolated_arrival_curve_T tsk)
have Rtsk := refine_task'.tsk : task_T Rtsk : refines (unify (A:=task_T) ==> Rtask)
taskT_to_task id
refines (prod_R Rnat (list_R (prod_R Rnat Rnat)))
(get_arrival_curve_prefix (taskT_to_task tsk))
(get_extrapolated_arrival_curve_T tsk)
rewrite refinesE in Rtsk.tsk : task_T Rtsk : (unify (A:=task_T) ==> Rtask)%rel taskT_to_task
id
refines (prod_R Rnat (list_R (prod_R Rnat Rnat)))
(get_arrival_curve_prefix (taskT_to_task tsk))
(get_extrapolated_arrival_curve_T tsk)
specialize (Rtsk tsk tsk (unifyxx _)); simpl in Rtsk.tsk : task_T Rtsk : Rtask (taskT_to_task tsk) tsk
refines (prod_R Rnat (list_R (prod_R Rnat Rnat)))
(get_arrival_curve_prefix (taskT_to_task tsk))
(get_extrapolated_arrival_curve_T tsk)
move : (refine_task_arrival) => Rab.tsk : task_T Rtsk : Rtask (taskT_to_task tsk) tsk Rab : refines (Rtask ==> Rtask_ab) task_arrival
task_arrival_T
refines (prod_R Rnat (list_R (prod_R Rnat Rnat)))
(get_arrival_curve_prefix (taskT_to_task tsk))
(get_extrapolated_arrival_curve_T tsk)
rewrite refinesE in Rab.tsk : task_T Rtsk : Rtask (taskT_to_task tsk) tsk Rab : (Rtask ==> Rtask_ab)%rel task_arrival
task_arrival_T
refines (prod_R Rnat (list_R (prod_R Rnat Rnat)))
(get_arrival_curve_prefix (taskT_to_task tsk))
(get_extrapolated_arrival_curve_T tsk)
specialize (Rab _ _ Rtsk).tsk : task_T Rtsk : Rtask (taskT_to_task tsk) tsk Rab : Rtask_ab (task_arrival (taskT_to_task tsk))
(task_arrival_T tsk)
refines (prod_R Rnat (list_R (prod_R Rnat Rnat)))
(get_arrival_curve_prefix (taskT_to_task tsk))
(get_extrapolated_arrival_curve_T tsk)
rewrite /get_arrival_curve_prefix /get_extrapolated_arrival_curve_T.tsk : task_T Rtsk : Rtask (taskT_to_task tsk) tsk Rab : Rtask_ab (task_arrival (taskT_to_task tsk))
(task_arrival_T tsk)
refines (prod_R Rnat (list_R (prod_R Rnat Rnat)))
match task_arrival (taskT_to_task tsk) with
| Periodic p => inter_arrival_to_prefix p
| Sporadic m => inter_arrival_to_prefix m
| ArrivalPrefix steps => steps
end
match task_arrival_T tsk with
| Periodic_T p =>
inter_arrival_to_extrapolated_arrival_curve_T p
| Sporadic_T m =>
inter_arrival_to_extrapolated_arrival_curve_T m
| ArrivalPrefix_T steps => steps
end
unfold inter_arrival_to_prefix, inter_arrival_to_extrapolated_arrival_curve_T.tsk : task_T Rtsk : Rtask (taskT_to_task tsk) tsk Rab : Rtask_ab (task_arrival (taskT_to_task tsk))
(task_arrival_T tsk)
refines (prod_R Rnat (list_R (prod_R Rnat Rnat)))
match task_arrival (taskT_to_task tsk) with
| Periodic p => (p, [:: (1 , 1 )])
| Sporadic m => (m, [:: (1 , 1 )])
| ArrivalPrefix steps => steps
end
match task_arrival_T tsk with
| Periodic_T p => (p, [:: (1 %C, 1 %C)])
| Sporadic_T m => (m, [:: (1 %C, 1 %C)])
| ArrivalPrefix_T steps => steps
end
destruct (task_arrival _) as [?|?|e], (task_arrival_T _) as [?|?|eT].tsk : task_T Rtsk : Rtask (taskT_to_task tsk) tsk n : nat n0 : binnat.N Rab : Rtask_ab (Periodic n) (Periodic_T n0)
refines (prod_R Rnat (list_R (prod_R Rnat Rnat)))
(n, [:: (1 , 1 )]) (n0, [:: (1 %C, 1 %C)])
all : try (inversion Rab; fail ).tsk : task_T Rtsk : Rtask (taskT_to_task tsk) tsk n : nat n0 : binnat.N Rab : Rtask_ab (Periodic n) (Periodic_T n0)
refines (prod_R Rnat (list_R (prod_R Rnat Rnat)))
(n, [:: (1 , 1 )]) (n0, [:: (1 %C, 1 %C)])
all : try (inversion Rab; subst ; refines_apply; fail ).tsk : task_T Rtsk : Rtask (taskT_to_task tsk) tsk e : ArrivalCurvePrefix eT : (binnat.N * seq (binnat.N * binnat.N))%type Rab : Rtask_ab (ArrivalPrefix e) (ArrivalPrefix_T eT)
refines (prod_R Rnat (list_R (prod_R Rnat Rnat))) e eT
destruct e as [h?], eT as [? st]; refines_apply; first by inversion Rab; subst ; tc.tsk : task_T Rtsk : Rtask (taskT_to_task tsk) tsk h : duration l : seq (duration * nat) n : binnat.N st : seq (binnat.N * binnat.N) Rab : Rtask_ab (ArrivalPrefix (h, l))
(ArrivalPrefix_T (n, st))
refines (list_R (prod_R Rnat Rnat)) l st
inversion Rab; subst .tsk : task_T Rtsk : Rtask (taskT_to_task tsk) tsk n : binnat.N st : seq (binnat.N * binnat.N) Rab : Rtask_ab (ArrivalPrefix (n, m_tb2tn st))
(ArrivalPrefix_T (n, st))
refines (list_R (prod_R Rnat Rnat)) (m_tb2tn st) st
elim : st Rab => [|a st IHst] Rab; first by rewrite //= refinesE; apply list_R_nil_R.tsk : task_T Rtsk : Rtask (taskT_to_task tsk) tsk n : binnat.N a : (binnat.N * binnat.N)%type st : seq (binnat.N * binnat.N) IHst : Rtask_ab (ArrivalPrefix (n, m_tb2tn st))
(ArrivalPrefix_T (n, st)) ->
refines (list_R (prod_R Rnat Rnat))
(m_tb2tn st) st Rab : Rtask_ab (ArrivalPrefix (n, m_tb2tn (a :: st)))
(ArrivalPrefix_T (n, a :: st))
refines (list_R (prod_R Rnat Rnat))
(m_tb2tn (a :: st)) (a :: st)
destruct a; rewrite //= refinesE.tsk : task_T Rtsk : Rtask (taskT_to_task tsk) tsk n, n0, n1 : binnat.N st : seq (binnat.N * binnat.N) IHst : Rtask_ab (ArrivalPrefix (n, m_tb2tn st))
(ArrivalPrefix_T (n, st)) ->
refines (list_R (prod_R Rnat Rnat))
(m_tb2tn st) st Rab : Rtask_ab
(ArrivalPrefix (n, m_tb2tn ((n0, n1) :: st)))
(ArrivalPrefix_T (n, (n0, n1) :: st))
list_R (prod_R Rnat Rnat)
(tb2tn (n0, n1) :: m_tb2tn st) ((n0, n1) :: st)
apply list_R_cons_R; first by apply refinesP; unfold tb2tn,tmap; refines_apply.tsk : task_T Rtsk : Rtask (taskT_to_task tsk) tsk n, n0, n1 : binnat.N st : seq (binnat.N * binnat.N) IHst : Rtask_ab (ArrivalPrefix (n, m_tb2tn st))
(ArrivalPrefix_T (n, st)) ->
refines (list_R (prod_R Rnat Rnat))
(m_tb2tn st) st Rab : Rtask_ab
(ArrivalPrefix (n, m_tb2tn ((n0, n1) :: st)))
(ArrivalPrefix_T (n, (n0, n1) :: st))
list_R (prod_R Rnat Rnat) (m_tb2tn st) st
by apply refinesP, IHst.
Qed .
(** Next, we prove a refinement for [sorted] when applied to [leq_steps]. *)
Global Instance refine_sorted_leq_steps :
forall tsk ,
refines (bool_R)%rel
(sorted leq_steps (steps_of (get_arrival_curve_prefix (taskT_to_task tsk))))
(sorted leq_steps_T (get_extrapolated_arrival_curve_T tsk).2 ) | 0 .forall tsk : task_T,
refines bool_R
(sorted leq_steps
(steps_of
(get_arrival_curve_prefix (taskT_to_task tsk))))
(sorted leq_steps_T
(get_extrapolated_arrival_curve_T tsk).2 )
Proof .forall tsk : task_T,
refines bool_R
(sorted leq_steps
(steps_of
(get_arrival_curve_prefix (taskT_to_task tsk))))
(sorted leq_steps_T
(get_extrapolated_arrival_curve_T tsk).2 )
intros .tsk : task_T
refines bool_R
(sorted leq_steps
(steps_of
(get_arrival_curve_prefix (taskT_to_task tsk))))
(sorted leq_steps_T
(get_extrapolated_arrival_curve_T tsk).2 )
by apply refine_leq_steps_sorted; refines_apply.
Qed .
(** Lastly, we prove a refinement for the task request-bound function. *)
Global Instance refine_task_rbf :
refines ( Rtask ==> Rnat ==> Rnat )%rel task_rbf task_rbf_T.refines (Rtask ==> Rnat ==> Rnat) task_rbf task_rbf_T
Proof .refines (Rtask ==> Rnat ==> Rnat) task_rbf task_rbf_T
apply refines_abstr2.forall (a : Task) (b : task_T),
refines Rtask a b ->
forall (a' : nat) (b' : binnat.N),
refines Rnat a' b' ->
refines Rnat (task_rbf a a') (task_rbf_T b b')
rewrite /task_rbf /task_rbf_T /task_request_bound_function
/concept.task_cost /TaskCost
/max_arrivals /MaxArrivals => t t' Rt y y' Ry.t : Task t' : task_T Rt : refines Rtask t t' y : nat y' : binnat.N Ry : refines Rnat y y'
refines Rnat (task_cost t * ConcreteMaxArrivals t y)
(task_cost_T t' * ConcreteMaxArrivals_T t' y')%C
by refines_apply.
Qed .
End Theory .