Library prosa.implementation.refinements.FP.refinements

Throughout this file, we work with Prosa's fixed-priority policy implementation.
#[local] Existing Instance NumericFPAscending.

We begin by defining a generic version of the functions we seek to define.
Section Definitions.

Consider a generic type T supporting basic arithmetic operations, neutral elements, and comparisons.
  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_of2 : eq_of (@task_T T)}.

We define a generic version of higher-or-equal priority task, ...
... of total request-bound function of higher-or-equal priority task, ...
  Definition total_hep_rbf_T (ts : seq task_T) (tsk : task_T) (Δ : T) : T :=
    let hep_ts := filter (fun tsk'hep_task_T tsk' tsk) ts in
    let work_ts := map (fun tsk'task_rbf_T tsk' Δ) hep_ts in
    foldr +%C 0%C work_ts.

... an analogous version of hep_task in without symmetry, ...
  Definition ohep_task_T tsk_o tsk :=
    (hep_task_T tsk_o tsk) && (~~ (eq_of2 tsk_o tsk)%C).

... with a respective cumulative version.
  Definition total_ohep_rbf_T (ts : seq task_T) (tsk : task_T) (Δ : T) : T :=
    let hep_ts := filter (fun tsk'ohep_task_T tsk' tsk) ts in
    let work_ts := map (fun tsk'task_rbf_T tsk' Δ) hep_ts in
    foldr +%C 0%C work_ts.

Next, we define a generic version of check_point_FP, ...
  Definition check_point_FP_T (ts : seq task_T) (tsk : task_T) (R : T) (P : T × T) : bool :=
    (task_rbf_T tsk (P.1 + 1) +
     total_ohep_rbf_T ts tsk (P.1 + P.2) P.1 + P.2)%C && (P.2 R)%C.

... a generic version of blocking_bound_NP, ...
  Definition blocking_bound_NP_T (ts : seq task_T) (tsk : task_T) :=
    let lp_ts := filter (fun tsk_o~~ hep_task_T tsk_o tsk) ts in
    let block_ts := map (fun tsk_otask_cost_T tsk_o - 1)%C lp_ts in
    foldr maxn_T 0%C block_ts.

... and of check_point_NP.
  Definition check_point_NP_T (ts : seq task_T) (tsk : task_T) (R : T) (P : T × T) : bool :=
    (blocking_bound_NP_T ts tsk
     + (task_rbf_T tsk (P.1 + 1) - (task_cost_T tsk - 1))
     + total_ohep_rbf_T ts tsk (P.1 + P.2) P.1 + P.2)%C
    && (P.2 + (task_cost_T tsk - 1) R)%C.

End Definitions.

In this section, we introduce some functions operating on binary numbers.
Section DefinitionsN.

We provide a definition of iota, ...
  Definition iota_N (a Δ : N) := iota_T a Δ.

  Definition search_space_emax_FP_h_N (tsk : task_T) (l r : N) : seq N :=
    let h := get_horizon_of_task_T tsk in
    let offsets := map (N.mul h) (iota_N l r) in
    let emax_offsets := repeat_steps_with_offset_T tsk offsets in
    map predn_T emax_offsets.

... and of search_space_emax_FP.
  Definition search_space_emax_FP_N (tsk : task_T) (L : N) :=
    let h := get_horizon_of_task_T tsk in
    search_space_emax_FP_h_N tsk 0 (((L %/ h)+1))%C.

End DefinitionsN.

Refinements

We now establish the desired refinements.
First, we prove a refinement for the search_space_emax_h function.
Local Instance refine_search_space_emax_h :
  refines (Rtask ==> Rnat ==> Rnat ==> list_R Rnat)%rel
          search_space_emax_FP_h
          search_space_emax_FP_h_N.

Next, we prove a refinement for the search_space_emax_FP function.
Global Instance refine_search_space_emax :
   tsk,
    refines (Rnat ==> list_R Rnat)%rel
            (search_space_emax_FP (taskT_to_task tsk))
            (search_space_emax_FP_N tsk).

Next, we prove a refinement for the hep_task function.
Global Instance refine_hep_task :
  refines ( Rtask ==> Rtask ==> bool_R )%rel hep_task hep_task_T.

Next, we prove a refinement for the total_hep_rbf function.
Global Instance refine_total_hep_rbf :
  refines ( list_R Rtask ==> Rtask ==> Rnat ==> Rnat )%rel total_hep_rbf total_hep_rbf_T.

Next, we prove a special-case refinement for the total_hep_rbf function when applied to a refined task set and a refined task. This special case is required to guide the typeclass engine.
Global Instance refine_total_hep_rbf' :
   ts tsk,
    refines (Rnat ==> Rnat)%rel
            (total_hep_rbf (map taskT_to_task ts) (taskT_to_task tsk))
            (total_hep_rbf_T ts tsk) | 0.

Next, we provide equality comparisons between different pairs of objects manipulated in Poet's certificates.
Global Instance eq_listN : eq_of (seq N) := fun x yx == y.
Global Instance eq_listNN : eq_of (seq (prod N N)) := fun x yx == y.
Global Instance eq_NlistNN : eq_of (prod N (seq (prod N N))) := fun x yx == y.
Global Instance eq_taskab : eq_of (@task_arrivals_bound_T N) := taskab_eqdef_T.
Global Instance eq_task : eq_of (@task_T N) := task_eqdef_T.

Next, we prove a refinement for the task_eqdef function.
Global Instance refine_task_eqdef :
  refines (Rtask ==> Rtask ==> bool_R)%rel task_eqdef task_eqdef_T.

Next, we prove a refinement for the ohep_task function.
Global Instance refine_ohep_task :
  refines ( Rtask ==> Rtask ==> bool_R )%rel ohep_task ohep_task_T.

Next, we prove a refinement for the total_ohep_rbf function.
Global Instance refine_total_ohep_rbf :
  refines ( list_R Rtask ==> Rtask ==> Rnat ==> Rnat )%rel total_ohep_rbf total_ohep_rbf_T.

Next, we prove a refinement for the check_point_FP function.
Global Instance refine_check_point :
  refines (list_R Rtask ==> Rtask ==> Rnat ==> prod_R Rnat Rnat ==> bool_R)%rel
          check_point_FP check_point_FP_T.

Next, we prove a special-case refinement for the check_point_FP function when applied to a refined task set and a refined task. This special case is required to guide the typeclass engine.
Global Instance refine_check_point' :
   ts tsk,
    refines (Rnat ==> prod_R Rnat Rnat ==> bool_R)%rel
            (check_point_FP (map taskT_to_task ts) (taskT_to_task tsk))
            (check_point_FP_T ts tsk) | 0.

Next, we prove a refinement for the blocking_bound_NP function.
Global Instance refine_blocking_bound :
  refines ( list_R Rtask ==> Rtask ==> Rnat )%rel blocking_bound_NP blocking_bound_NP_T.

Next, we prove a special-case refinement for the blocking_bound_NP function when applied to a refined task set and a refined task. This special case is required to guide the typeclass engine.
Global Instance refine_blocking_bound' :
   ts tsk,
    refines ( Rnat )%rel
            (blocking_bound_NP (map taskT_to_task ts) (taskT_to_task tsk))
            (blocking_bound_NP_T ts tsk) | 0.

Next, we prove a refinement for the check_point_NP function.
Global Instance refine_check_point_NP :
  refines (list_R Rtask ==> Rtask ==> Rnat ==> prod_R Rnat Rnat ==> bool_R)%rel
          check_point_NP check_point_NP_T.

Finally, we prove a special-case refinement for the check_point_NP function when applied to a refined task set and a refined task. This special case is required to guide the typeclass engine.
Global Instance refine_check_point_NP' :
   ts tsk,
    refines (Rnat ==> prod_R Rnat Rnat ==> bool_R)%rel
            (check_point_NP (map taskT_to_task ts) (taskT_to_task tsk))
            (check_point_NP_T ts tsk) | 0.