Link NC arrival_curves to Prosa's Request Bound Functions

An overapproximation is provided in one direction,
the converse direction works only for periodic clocks.

_CoqProject

@@ -17,5 +17,6 @@ examples/case_study/arbitrary_flows.v
 #examples/case_study/case.v  # needs minerve to compile
 link/clock.v
 link/flow_cc_of_arrival_sequence.v
+link/arrival_curve_of_request_bound_function.v
 
 COQDOCFLAGS = "-g -interpolate -utf8 --external https://math-comp.github.io/htmldoc/ mathcomp -R . NCCoq"

link/arrival_curve_of_request_bound_function.v

+From mathcomp Require Import ssreflect ssrfun ssrbool eqtype order ssrnat ssrint.
+From mathcomp Require Import choice seq path bigop ssralg ssrnum rat.
+From mathcomp Require Import fintype finfun.
+From mathcomp.analysis Require Import reals ereal nngnum posnum boolp classical_sets.
+Require Import prosa.util.nat prosa.util.bigcat prosa.util.sum.
+Require Import prosa.model.task.concept prosa.behavior.arrival_sequence.
+Require Import prosa.model.task.arrival.request_bound_functions.
+Require Import RminStruct cumulative_curves arrival_curves.
+Require Import clock flow_cc_of_arrival_sequence.
+
+Set Implicit Arguments.
+Unset Strict Implicit.
+Unset Printing Implicit Defensive.
+
+Local Open Scope classical_set_scope.
+Local Open Scope ring_scope.
+
+Import Order.Theory GRing.Theory Num.Theory DualAddTheory.
+
+Section Arrival_curve_of_request_bound_function.
+
+Context {Task : TaskType}.
+Context {Job : JobType}.
+Context `{JobTask Job Task}.
+Context `{JobCost Job}.
+
+(** Note that this is tight for periodic clocks
+    but can be conservative otherwise. *)
+Program Definition arrival_curve_of_request_bound_function
+        (rbf : duration -> nat) (c : uclock) : Fplus :=
+  Build_Fplus
+    (fun d => (rbf `|ceil (d%:nngnum / (uclock_min_intertick c)%:num)|%nat)%:R%:E) _.
+Next Obligation. by apply/leFP => t; rewrite lee_fin. Qed.
+
+Program Definition arrival_curve_of_valid_request_bound_function
+        (rbf : duration -> nat) (valid_rbf : valid_request_bound_function rbf)
+        (c : uclock) : Fup :=
+  Build_Fup (arrival_curve_of_request_bound_function rbf c) _.
+Next Obligation.
+apply/asboolP => x y xley.
+rewrite lee_fin ler_nat; apply: (proj2 valid_rbf).
+rewrite -lez_nat !gez0_abs; [|exact/ceil_ge0/divr_ge0..].
+by apply: le_ceil; rewrite ler_pmul2r.
+Qed.
+
+Lemma arrival_curve_of_request_bound_function_is_maximal_arrival_any_clock
+      (c : uclock) (tsk : Task) (arr : arrival_sequence Job) f
+      (rbf : duration -> nat) :
+  related_arrival_flow_cc c tsk arr f ->
+  valid_request_bound_function rbf ->
+  respects_max_request_bound arr tsk rbf ->
+  is_maximal_arrival f (arrival_curve_of_request_bound_function rbf c).
+Proof.
+move=> -> [_ Vrbf] Hrbf t d /=.
+set ct := next_tick c t.
+set ctd := next_tick c (t%:nngnum + d%:nngnum)%:nng.
+rewrite -daddEFin lee_fin ler_subl_addl -natrD ler_nat.
+have ctlectd : (ct <= ctd)%nat.
+{ by apply: next_tick_leq; rewrite /= ler_addl. }
+rewrite /arrivals_between.
+rewrite (big_cat_nat _ _ _ _ ctlectd) //= filter_cat big_cat /= leq_add2l.
+apply/(leq_trans (Hrbf _ _ ctlectd))/Vrbf.
+rewrite -lez_nat gez0_abs; [|exact/ceil_ge0/divr_ge0].
+exact: next_tick_incr_ub.
+Qed.
+
+(** The above can be specialized to periodic clocks *)
+Lemma arrival_curve_of_request_bound_function_is_maximal_arrival
+      (T : {posnum R}) (tsk : Task) (arr : arrival_sequence Job) f
+      (rbf : duration -> nat) :
+  related_arrival_flow_cc (periodic_uclock T) tsk arr f ->
+  valid_request_bound_function rbf ->
+  respects_max_request_bound arr tsk rbf ->
+  is_maximal_arrival
+    f (arrival_curve_of_request_bound_function rbf (periodic_uclock T)).
+Proof.
+exact: arrival_curve_of_request_bound_function_is_maximal_arrival_any_clock.
+Qed.
+
+(** The converse holds only for periodic clocks *)
+Lemma arrival_curve_of_request_bound_function_respects_max_request_bound
+      (T : {posnum R}) (tsk : Task) (arr : arrival_sequence Job) f
+      (rbf : duration -> nat) :
+  related_arrival_flow_cc (periodic_uclock T) tsk arr f ->
+  valid_request_bound_function rbf ->
+  is_maximal_arrival
+    f (arrival_curve_of_request_bound_function rbf (periodic_uclock T)) ->
+  respects_max_request_bound arr tsk rbf.
+Proof.
+set c := periodic_uclock T.
+move=> -> [_ Vrbf] Halpha t1 t2 Ht1t2.
+pose t := c t1.
+have Pd : 0 <= (c t2)%:nngnum - t%:nngnum.
+{ rewrite subr_ge0; exact: uclock_le. }
+pose d := Nonneg.NngNum _ Pd.
+move: (Halpha t d).
+rewrite -daddEFin lee_fin ler_subl_addl -natrD ler_nat -leq_subLR.
+rewrite (_ : _%:nng = c t2); [|by apply/val_inj; rewrite /= addrCA addrA addrK].
+rewrite /t !uclockK.
+rewrite /arrivals_between.
+rewrite (big_cat_nat _ _ _ _ Ht1t2) //= filter_cat big_cat /= addKn => H'.
+apply/(leq_trans H')/Vrbf.
+rewrite -mulrBl -mulrA divff// mulr1 -natrB//.
+rewrite -lez_nat gez0_abs; [|exact: ceil_ge0].
+rewrite -(ler_int R) -RceilE.
+by rewrite pmulrn /Rceil -mulrNz Rfloor_natz mulrNz opprK.
+Qed.
+
+End Arrival_curve_of_request_bound_function.

link/clock.v

@@ -120,6 +120,17 @@ apply: le_lt_trans (uclock_lt_next_tick ct'ltct).
 exact: uclock_next_tick_gt.
 Qed.
 
+Lemma next_tick_leqS (c : uclock) (t t' : {nonneg R}) :
+  t%:nngnum <= t'%:nngnum + (uclock_min_intertick c)%:num ->
+  (next_tick c t <= (next_tick c t').+1)%nat.
+Proof.
+move=> tlet'eps; rewrite leqNgt; apply/negP => /uclock_lt_next_tick ntlt.
+move: tlet'eps; apply/negP; rewrite -ltNge.
+apply: le_lt_trans ntlt.
+apply: le_trans (uclock_incr _ _); rewrite ler_add2r.
+exact: uclock_next_tick_gt.
+Qed.
+
 Lemma uclockK (c : uclock) : cancel c (next_tick c).
 Proof.
 rewrite /next_tick => n.
@@ -147,6 +158,37 @@ move: tgt0; apply/negP; rewrite -leNgt.
 by apply: (le_trans (uclock_next_tick_gt c t)); rewrite nt0 uclock_0.
 Qed.
 
+Lemma next_tick_incr_ub (c : uclock) (t d : {nonneg R}) :
+  (next_tick c (t%:nngnum + d%:nngnum)%:nng%R - next_tick c t)%nat
+  <= ceil (d%:nngnum / (uclock_min_intertick c)%:num) :> int.
+Proof.
+set eps := uclock_min_intertick c.
+set ddeps := ceil _.
+have: d%:nngnum <= eps%:num * ddeps%:~R.
+{ by rewrite mulrC -ler_pdivr_mulr// -RceilE Rceil_ge. }
+case ddepsE: ddeps => [n|n] dlem.
+2:{ exfalso; move: (le_refl (0 : R)); apply/negP; rewrite -ltNge.
+  apply: (@le_lt_trans _ _ d%:nngnum) => [//|].
+  by apply: (le_lt_trans dlem); rewrite pmulr_rlt0// ltrz0. }
+rewrite lez_nat leq_subLR.
+elim: n {ddeps ddepsE} d dlem => [d|n IHn d dlem].
+{ rewrite mulr0 => dle0.
+  rewrite (_ : _%:nng = t) ?addn0//; apply/val_inj => /=.
+  by rewrite (_ : d%:nngnum = 0) ?addr0//; apply/le_anti; rewrite dle0 /=. }
+have [dleeps | epsltd] := leP d%:nngnum eps%:num.
+{ rewrite -addn1 addnCA; apply: leq_trans (leq_addl _ _); rewrite addn1.
+  by apply: next_tick_leqS; rewrite /= ler_add2l. }
+set td := _%:nng.
+pose dmeps := insubd 0%:nng (d%:nngnum - eps%:num).
+have tdleeps : td%:nngnum <= t%:nngnum + dmeps%:nngnum + eps%:num.
+{ by rewrite insubdK; [rewrite addrA subrK|rewrite /in_mem /= subr_ge0 ltW]. }
+apply: (leq_trans (next_tick_leqS tdleeps)).
+rewrite -(addn1 n) addnA addn1 ltnS; apply: IHn.
+rewrite insubdK; [|by rewrite /in_mem /= subr_ge0 ltW].
+rewrite ler_subl_addl; apply: (le_trans dlem).
+by rewrite -add1n PoszD intrD mulrDr mulr1.
+Qed.
+
 (** ** A few specific clocks *)
 
 (** Periodic clocks are a simple example of clock *)