analysis/abstract/iw_auxiliary.v

+Require Export prosa.analysis.definitions.interference.
+Require Export prosa.analysis.definitions.task_schedule.
+Require Export prosa.analysis.facts.priority.classes.
+Require Export prosa.analysis.abstract.restricted_supply.busy_prefix.
+Require Export prosa.model.aggregate.service_of_jobs.
+Require Export prosa.analysis.facts.model.service_of_jobs.
+
+
+(** * Auxiliary Lemmas About Interference and Interfering Workload. *)
+
+(** In this file we provide a set of auxiliary lemmas about generic
+    properties of Interference and Interfering Workload. *)
+Section InterferenceAndInterferingWorkloadAuxiliary.
+
+  (** 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}.
+
+  (** Assume we are provided with abstract functions for interference
+      and interfering workload. *)
+  Context `{Interference Job}.
+  Context `{InterferingWorkload Job}.
+
+  (** Consider any kind of fully supply-consuming uniprocessor model. *)
+  Context `{PState : ProcessorState Job}.
+  Hypothesis H_uniprocessor_proc_model : uniprocessor_model PState.
+  Hypothesis H_consumed_supply_proc_model : fully_consuming_proc_model PState.
+
+  (** Consider any valid arrival sequence with consistent arrivals ... *)
+  Variable arr_seq : arrival_sequence Job.
+  Hypothesis H_valid_arrival_sequence : valid_arrival_sequence arr_seq.
+
+  (** ... and any uni-processor schedule of this arrival
+      sequence ... *)
+  Variable sched : schedule PState.
+  Hypothesis H_jobs_come_from_arrival_sequence :
+    jobs_come_from_arrival_sequence sched arr_seq.
+
+  (** ... where jobs do not execute before their arrival or after
+      completion. *)
+  Hypothesis H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched.
+  Hypothesis H_completed_jobs_dont_execute : completed_jobs_dont_execute sched.
+
+  (** Let [tsk] be any task. *)
+  Variable tsk : Task.
+
+  (** For convenience, we define a function that "folds" cumulative
+      conditional interference with a predicate [fun _ _ => true] to
+      cumulative (unconditional) interference. *)
+  Lemma fold_cumul_interference :
+    forall j t1 t2,
+      cumul_cond_interference (fun _ _ => true) j t1 t2
+      = cumulative_interference j t1 t2.
+  Proof. by rewrite /cumulative_interference. Qed.
+
+  (** In this section, we prove a few basic properties of conditional
+      interference w.r.t. a generic predicate [P]. *)
+  Section CondInterferencePredicate.
+
+    (** In the following, consider a predicate [P]. *)
+    Variable P : Job -> instant -> bool.
+
+    (** First, we show that the cumulative conditional interference
+        within a time interval <<[t1, t2)>> can be rewritten as a sum
+        over all time instances satisfying [P j]. *)
+    Lemma cumul_cond_interference_alt :
+      forall j t1 t2,
+        cumul_cond_interference P j t1 t2 = \sum_(t1 <= t < t2 | P j t) interference j t.
+    Proof.
+      move=> j t1 t2; rewrite [RHS]big_mkcond //=; apply eq_big_nat => t _.
+      by rewrite /cond_interference; case: (P j t).
+    Qed.
+
+    (** Next, we show that cumulative interference on an interval
+        <<[al, ar)>> is bounded by the cumulative interference on an
+        interval <<[bl,br)>> if <<[al,ar)>> ⊆ <<[bl,br)>>. *)
+    Lemma cumulative_interference_sub :
+      forall (j : Job) (al ar bl br : instant),
+        bl <= al ->
+        ar <= br ->
+        cumul_cond_interference P j al ar <= cumul_cond_interference P j bl br.
+    Proof.
+      move => j al ar bl br LE1 LE2.
+      rewrite !cumul_cond_interference_alt.
+      case: (leqP al ar) => [LEQ|LT]; last by rewrite big_geq.
+      rewrite [leqRHS](@big_cat_nat _ _ _ al) //=; last by lia.
+      by rewrite [in X in _ <= _ + X](@big_cat_nat _ _ _ ar) //=; lia.
+    Qed.
+
+    (** We show that the cumulative interference of a job can be split
+        into disjoint intervals. *)
+    Lemma cumulative_interference_cat :
+      forall j t t1 t2,
+        t1 <= t <= t2 ->
+        cumul_cond_interference P j t1 t2
+        = cumul_cond_interference P j t1 t + cumul_cond_interference P j t t2.
+    Proof.
+      move => j t t1 t2 /andP [LE1 LE2].
+      by rewrite !cumul_cond_interference_alt {1}(@big_cat_nat _ _ _ t) //=.
+    Qed.
+
+  End CondInterferencePredicate.
+
+  (** Next, we show a few relations between interference functions
+      conditioned on different predicates. *)
+  Section CondInterferenceRelation.
+
+    (** Consider predicates [P1, P2]. *)
+    Variables P1 P2 : Job -> instant -> bool.
+
+    (** We introduce a lemma (similar to ssreflect's [bigID] lemma)
+        that allows us to split the cumulative conditional
+        interference w.r.t predicate [P1] into a sum of two cumulative
+        conditional interference w.r.t. predicates [P1 && P2] and [P1
+        && ~~ P2], respectively. *)
+    Lemma cumul_cond_interference_ID :
+      forall j t1 t2,
+        cumul_cond_interference P1 j t1 t2
+        = cumul_cond_interference (fun j t => P1 j t && P2 j t) j t1 t2
+          + cumul_cond_interference (fun j t => P1 j t && ~~ P2 j t) j t1 t2.
+    Proof.
+      move=> j t1 t2.
+      rewrite -big_split //=; apply eq_bigr => t _.
+      rewrite /cond_interference.
+      by case (P1 _ _), (P2 _ _ ), (interference _ _).
+    Qed.
+
+    (** If two predicates [P1] and [P2] are equivalent, then they can
+        be used interchangeably with [cumul_cond_interference]. *)
+    Lemma cumul_cond_interference_pred_eq :
+      forall (j : Job) (t1 t2 : instant),
+        (forall j t, P1 j t <-> P2 j t) ->
+        cumul_cond_interference P1 j t1 t2
+        = cumul_cond_interference P2 j t1 t2.
+    Proof.
+      move=> j t1 t2 EQU.
+      apply eq_bigr => t _; rewrite /cond_interference.
+      move: (EQU j t).
+      by case (P1 j t), (P2 j t), (interference _ _); move=> CONTR => //=; exfalso; apply notF, CONTR.
+    Qed.
+
+  End CondInterferenceRelation.
+
+End InterferenceAndInterferingWorkloadAuxiliary.

analysis/abstract/lower_bound_on_service.v

+Require Export prosa.analysis.facts.model.service_of_jobs.
+Require Export prosa.analysis.facts.preemption.rtc_threshold.job_preemptable.
+Require Export prosa.analysis.abstract.definitions.
+Require Export prosa.analysis.abstract.busy_interval.
+
+(** * Lower Bound On Job Service *)
+(** In this section we prove that if the cumulative interference
+    inside a busy interval is bounded by a certain constant then a job
+    executes long enough to reach a specified amount of service. *)
+Section LowerBoundOnService.
+
+  (** 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}.
+
+  (** In addition, we assume existence of a function mapping jobs to
+      their preemption points. *)
+  Context `{JobPreemptable Job}.
+
+  (** Consider _any_ kind of processor state model. *)
+  Context {PState : ProcessorState Job}.
+
+  (** Consider any arrival sequence with consistent arrivals ... *)
+  Variable arr_seq : arrival_sequence Job.
+  Hypothesis H_arrival_times_are_consistent : consistent_arrival_times arr_seq.
+
+  (** ... and any schedule of this arrival sequence. *)
+  Variable sched : schedule PState.
+
+  (** Assume that the job costs are no larger than the task costs. *)
+  Hypothesis H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs arr_seq.
+
+  (** Let [tsk] be any task that is to be analyzed. *)
+  Variable tsk : Task.
+
+  (** Assume we are provided with abstract functions for interference
+      and interfering workload. *)
+  Context `{Interference Job}.
+  Context `{InterferingWorkload Job}.
+
+  (** We assume that the schedule is work-conserving. *)
+  Hypothesis H_work_conserving : work_conserving arr_seq sched.
+
+  (** Let [j] be any job of task [tsk] with positive cost. *)
+  Variable j : Job.
+  Hypothesis H_j_arrives : arrives_in arr_seq j.
+  Hypothesis H_job_of_tsk : job_of_task tsk j.
+  Hypothesis H_job_cost_positive : job_cost_positive j.
+
+  (** In this section, we show that the cumulative interference is a
+      complement to the total time where job [j] is scheduled inside a
+      busy interval prefix. *)
+  Section InterferenceIsComplement.
+
+    (** Consider any busy interval prefix <<[t1, t2)>> of job [j]. *)
+    Variable t1 t2 : instant.
+    Hypothesis H_busy_interval : busy_interval_prefix sched j t1 t2.
+
+    (** Consider any sub-interval <<[t, t + δ)>> inside the busy interval <<[t1, t2)>>. *)
+    Variables (t : instant) (δ : duration).
+    Hypothesis H_t1_le_t : t1 <= t.
+    Hypothesis H_tδ_le_t2 : t + δ <= t2.
+
+    (** We prove that sum of cumulative service and cumulative
+        interference in the interval <<[t, t + δ)>> is equal to
+        [δ]. *)
+    Lemma interference_is_complement_to_schedule :
+      service_during sched j t (t + δ) + cumulative_interference j t (t + δ) >= δ.
+    Proof.
+      rewrite /service_during /cumulative_interference /cumul_cond_interference /service_at.
+      rewrite -big_split //= -{1}(sum_of_ones t δ) big_nat [in X in _ <= X]big_nat leq_sum // => x /andP[Lo Hi].
+      move: (H_work_conserving j t1 t2 x) => Workj.
+      feed_n 4 Workj => //; first by lia.
+      rewrite /cond_interference //=.
+      case INT: interference; first by lia.
+      by rewrite // addn0; apply Workj; rewrite INT.
+    Qed.
+    
+    (** Also, note that under the unit-service processor model
+        assumption, the sum of service within the interval <<[t, t + δ)>> 
+        and the cumulative interference within the same interval
+        is bounded by the length of the interval (i.e., [δ]).  *) 
+    Remark service_and_interference_bounded :
+      unit_service_proc_model PState ->
+      service_during sched j t (t + δ) + cumulative_interference j t (t + δ) <= δ.
+    Proof.
+      move => UNIT.
+      rewrite /service_during /cumulative_interference/service_at -big_split //=.
+      rewrite -{2}(sum_of_ones t δ).
+      rewrite big_nat [in X in _ <= X]big_nat; apply leq_sum => x /andP[Lo Hi].
+      move: (H_work_conserving j t1 t2 x) => Workj.
+      feed_n 4 Workj => //.
+      { by apply/andP; split; lia. }
+      rewrite /cond_interference //=.
+      destruct interference.
+      - rewrite addn1 ltnS.
+        by move_neq_up NE; apply Workj.
+      - by rewrite addn0; apply UNIT.
+    Qed.
+    
+  End InterferenceIsComplement.
+
+  (** In this section, we prove a sufficient condition under which job
+      [j] receives enough service. *)
+  Section InterferenceBoundedImpliesEnoughService.
+
+    (** Consider any busy interval <<[t1, t2)>> of job [j]. *)
+    Variable t1 t2 : instant.
+    Hypothesis H_busy_interval : busy_interval sched j t1 t2.
+
+    (** Let [progress_of_job] be the desired service of job [j]. *)
+    Variable progress_of_job : duration.
+    Hypothesis H_progress_le_job_cost : progress_of_job <= job_cost j.
+
+    (** Assume that for some [δ] the sum of desired progress and
+        cumulative interference is bounded by [δ]. *)
+    Variable δ : duration.
+    Hypothesis H_total_workload_is_bounded :
+      progress_of_job + cumulative_interference j t1 (t1 + δ) <= δ.
+
+    (** Then, it must be the case that the job has received no less
+        service than [progress_of_job]. *)
+    Theorem j_receives_enough_service :
+      service sched j (t1 + δ) >= progress_of_job.
+    Proof.
+      destruct (leqP (t1 + δ) t2) as [NEQ|NEQ]; last first.
+      { move: (job_completes_within_busy_interval _ _ _ _ H_busy_interval) => COMPL.
+        apply leq_trans with (job_cost j) => [//|].
+        rewrite /service -(service_during_cat _ _ _ t2); last by apply/andP; split; last apply ltnW.
+        by apply leq_trans with (service_during sched j 0 t2); [| rewrite leq_addr].
+      }
+      { move: H_total_workload_is_bounded => BOUND.
+        rewrite addnC in BOUND; apply leq_subRL_impl in BOUND.
+        apply leq_trans with (δ - cumulative_interference j t1 (t1 + δ)) => [//|].
+        apply leq_trans with (service_during sched j t1 (t1 + δ)).
+        - eapply leq_trans.
+          + by apply leq_sub2r, (interference_is_complement_to_schedule t1 t2);
+              [apply H_busy_interval | apply leqnn | apply NEQ].
+          + by rewrite -addnBA // subnn addn0 //.
+        - rewrite /service -[X in _ <= X](service_during_cat _ _ _ t1); first by rewrite leq_addl //.
+          by apply/andP; split; last rewrite leq_addr.
+      }
+    Qed.
+
+  End InterferenceBoundedImpliesEnoughService.
+
+End LowerBoundOnService.

analysis/abstract/restricted_supply/abstract_rta.v

+Require Export prosa.analysis.facts.behavior.supply.
+Require Export prosa.analysis.facts.SBF.
+Require Export prosa.analysis.abstract.abstract_rta.
+Require Export prosa.analysis.abstract.iw_auxiliary.
+Require Export prosa.analysis.abstract.IBF.supply.
+Require Export prosa.analysis.abstract.restricted_supply.busy_sbf.
+
+(** * Abstract Response-Time Analysis for Restricted-Supply Processors (aRSA) *)
+(** In this section we propose a general framework for response-time
+    analysis ([RTA]) for real-time tasks with arbitrary arrival models
+    under uni-processor scheduling subject to supply restrictions,
+    characterized by a given [SBF]. *)
+
+(** We prove that the maximum (with respect to the set of offsets)
+    among the solutions of the response-time bound recurrence is a
+    response-time bound for [tsk]. Note that in this section we add
+    additional restrictions on the processor state. These assumptions
+    allow us to eliminate the second equation from [aRTA+]'s
+    recurrence since jobs experience delays only due to the lack of
+    supply while executing non-preemptively. *)
+Section AbstractRTARestrictedSupply.
+
+  (** Consider any type of tasks with a run-to-completion threshold ... *)
+  Context {Task : TaskType}.
+  Context `{TaskCost Task}.
+  Context `{TaskRunToCompletionThreshold Task}.
+
+  (**  ... and any type of jobs associated with these tasks. *)
+  Context {Job : JobType}.
+  Context `{JobTask Job Task}.
+  Context `{JobArrival Job}.
+  Context `{JobCost Job}.
+  Context `{JobPreemptable Job}.
+
+  (** Consider any kind of fully supply-consuming unit-supply
+      processor state model. *)
+  Context `{PState : ProcessorState Job}.
+  Hypothesis H_unit_supply_proc_model : unit_supply_proc_model PState.
+  Hypothesis H_consumed_supply_proc_model : fully_consuming_proc_model PState.
+
+  (** Consider any valid arrival sequence. *)
+  Variable arr_seq : arrival_sequence Job.
+  Hypothesis H_valid_arrivals : valid_arrival_sequence arr_seq.
+
+  (** Consider any restricted supply uniprocessor schedule of this
+      arrival sequence ...*)
+  Variable sched : schedule PState.
+  Hypothesis H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched arr_seq.
+
+  (** ... where jobs do not execute before their arrival nor after completion. *)
+  Hypothesis H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched.
+  Hypothesis H_completed_jobs_dont_execute : completed_jobs_dont_execute sched.
+
+  (** Assume we are given valid WCETs for all tasks.  *)
+  Hypothesis H_valid_job_cost :
+    arrivals_have_valid_job_costs arr_seq.
+
+  (** Consider a task set [ts]... *)
+  Variable ts : list Task.
+
+  (** ... and a task [tsk] of [ts] that is to be analyzed. *)
+  Variable tsk : Task.
+  Hypothesis H_tsk_in_ts : tsk \in ts.
+
+  (** Consider a valid preemption model ... *)
+  Hypothesis H_valid_preemption_model : valid_preemption_model arr_seq sched.
+
+  (** ...and a valid task run-to-completion threshold function. That
+      is, [task_rtc tsk] is (1) no bigger than [tsk]'s cost and (2)
+      for any job [j] of task [tsk] [job_rtct j] is bounded by
+      [task_rtct tsk]. *)
+  Hypothesis H_valid_run_to_completion_threshold :
+    valid_task_run_to_completion_threshold arr_seq tsk.
+
+  (** Assume we are provided with abstract functions for Interference
+      and Interfering Workload. *)
+  Context `{Interference Job}.
+  Context `{InterferingWorkload Job}.
+
+  (** We assume that the scheduler is work-conserving. *)
+  Hypothesis H_work_conserving : work_conserving arr_seq sched.
+
+  (** Let [L] be a constant that bounds any busy interval of task [tsk]. *)
+  Variable L : duration.
+  Hypothesis H_busy_interval_exists :
+    busy_intervals_are_bounded_by arr_seq sched tsk L.
+
+  (** Consider a unit SBF valid in busy intervals (w.r.t. task
+      [tsk]). That is, (1) [SBF 0 = 0], (2) for any duration [Δ], the
+      supply produced during a busy-interval prefix of length [Δ] is
+      at least [SBF Δ], and (3) [SBF] makes steps of at most one. *)
+  Context {SBF : SupplyBoundFunction}.
+  Hypothesis H_valid_SBF : valid_busy_sbf arr_seq sched tsk SBF.
+  Hypothesis H_unit_SBF : unit_supply_bound_function SBF.
+
+  (** Next, we assume that [intra_IBF] is a bound on the intra-supply
+      interference incurred by task [tsk]. *)
+  Variable intra_IBF : duration -> duration -> duration.
+  Hypothesis H_intra_supply_interference_is_bounded :
+    intra_interference_is_bounded_by arr_seq sched tsk intra_IBF.
+
+  (** Given any job [j] of task [tsk] that arrives exactly [A] units
+      after the beginning of the busy interval, the bound on the
+      interference incurred by [j] within an interval of length [Δ] is
+      no greater than [(Δ - SBF Δ) + intra_IBF A Δ]. *)
+  Let IBF_P (A Δ : duration) :=
+    (Δ - SBF Δ) + intra_IBF A Δ.
+
+  (** Next, we instantiate function [IBF_NP], which is a function that
+      bounds interference in a non-preemptive stage of execution. We
+      prove that this function can be instantiated as [λ tsk F Δ ⟹ (F
+      - task_rtct tsk) + (Δ - SBF Δ - (F - SBF F))]. *)
+
+  (** Let us reiterate on the intuitive interpretation of this
+      function. Since [F] is a solution to the first equation
+      [task_rtct tsk + IBF_P A F <= F], we know that by time
+      instant [t1 + F] a job receives [task_rtct tsk] units of service
+      and, hence, it becomes non-preemptive. Knowing this information,
+      how can we bound the job's interference in an interval <<[t1, t1
+      + Δ)>>?  Note that this interval starts with the beginning of
+      the busy interval. We know that the job receives [F - task_rtct
+      tsk] units of interference. In the non-preemptive mode, a job
+      under analysis can still experience some interference due to a
+      lack of supply. This interference is bounded by [(Δ - SBF Δ) -
+      (F - SBF F)] since part of this interference has already been
+      accounted for in the preemptive part of the execution ([F - SBF
+      F]). *)
+  Let IBF_NP (F Δ : duration) :=
+    (F - task_rtct tsk) + (Δ - SBF Δ - (F - SBF F)).
+
+  (** In the next section, we prove a few helper lemmas. *)
+  Section AuxiliaryLemmas.
+
+      (** Consider any job [j] of [tsk]. *)
+      Variable j : Job.
+      Hypothesis H_j_arrives : arrives_in arr_seq j.
+      Hypothesis H_job_of_tsk : job_of_task tsk j.
+      Hypothesis H_job_cost_positive : job_cost_positive j.
+
+      (** Consider the busy interval <<[t1, t2)>> of job [j]. *)
+      Variable t1 t2 : instant.
+      Hypothesis H_busy_interval : busy_interval_prefix sched j t1 t2.
+
+      (** Let's define [A] as a relative arrival time of job [j] (with
+          respect to time [t1]). *)
+      Let A : duration := job_arrival j - t1.
+
+      (** Consider an arbitrary time [Δ] ... *)
+      Variable Δ : duration.
+      (** ... such that [t1 + Δ] is inside the busy interval... *)
+      Hypothesis H_inside_busy_interval : t1 + Δ < t2.
+      (** ... the job [j] is not completed by time [(t1 + Δ)]. *)
+      Hypothesis H_job_j_is_not_completed : ~~ completed_by sched j (t1 + Δ).
+
+      (** First, we show that blackout is counted as interference. *)
+      Lemma blackout_impl_interference :
+        forall t,
+          t1 <= t < t2 ->
+          is_blackout sched t ->
+          interference j t.
+      Proof.
+        move=> t /andP [LE1 LE2].
+        apply contraLR => /negP INT.
+        eapply H_work_conserving in INT =>//; last by lia.
+        by apply/negPn; eapply pos_service_impl_pos_supply.
+      Qed.
+
+      (** Next, we show that interference is equal to a sum of two
+          functions: [is_blackout] and [intra_interference]. *)
+      Lemma blackout_plus_local_is_interference :
+        forall t,
+          t1 <= t < t2 ->
+          is_blackout sched t + intra_interference sched j t
+          = interference j t.
+      Proof.
+        move=> t t_INT.
+        rewrite /intra_interference /cond_interference.
+        destruct (is_blackout sched t) eqn:BLACKOUT; rewrite (negbRL BLACKOUT) //.
+        by rewrite blackout_impl_interference.
+      Qed.
+
+      (** As a corollary, cumulative interference during a time
+          interval <<[t1, t1 + Δ)>> can be split into a sum of total
+          blackouts in <<[t1, t1 + Δ)>> and cumulative intra-supply
+          interference during <<[t1, t1 + Δ)>>. *)
+      Corollary blackout_plus_local_is_interference_cumul :
+        blackout_during sched t1 (t1 + Δ) + cumul_intra_interference sched j t1 (t1 + Δ)
+        = cumulative_interference j t1 (t1 + Δ).
+      Proof.
+        rewrite -big_split; apply eq_big_nat => //=.
+        move=> t /andP [t_GEQ t_LTN_td].
+        move: (ltn_trans t_LTN_td H_inside_busy_interval) => t_LTN_t2.
+        by apply blackout_plus_local_is_interference; apply /andP.
+      Qed.
+
+      (** Moreover, since the total blackout duration in an interval
+          of length [Δ] is bounded by [Δ - SBF Δ], the cumulative
+          interference during the time interval <<[t1, t1 + Δ)>> is
+          bounded by the sum of [Δ - SBF Δ] and cumulative
+          intra-supply interference during <<[t1, t1 + Δ)>>. *)
+      Corollary cumulative_job_interference_bound :
+        cumulative_interference j t1 (t1 + Δ)
+        <= (Δ - SBF Δ) + cumul_intra_interference sched j t1 (t1 + Δ).
+      Proof.
+        rewrite -blackout_plus_local_is_interference_cumul leq_add2r.
+        by eapply blackout_during_bound with (t2 := t2) => //.
+      Qed.
+
+      (** Next, consider a duration [F] such that [F <= Δ] and job [j]
+          has enough service to become non-preemptive by time instant
+          [t1 + F]. *)
+      Variable F : duration.
+      Hypothesis H_F_le_Δ : F <= Δ.
+      Hypothesis H_enough_service : task_rtct tsk <= service sched j (t1 + F).
+
+      (** Then, we show that job [j] does not experience any
+          intra-supply interference in the time interval <<[t1 + F, t1 +
+          Δ)>>. *)
+      Lemma no_intra_interference_after_F :
+        cumul_intra_interference sched j (t1 + F) (t1 + Δ) = 0.
+      Proof.
+        rewrite /cumul_intra_interference/ cumul_cond_interference big_nat.
+        apply big1; move => t /andP [GE__t LT__t].
+        apply/eqP; rewrite eqb0; apply/negP.
+        move => /andP [P /negPn /negP D]; apply: D; apply/negP.
+        eapply H_work_conserving with (t1 := t1) (t2 := t2); eauto 2.
+        { by apply/andP; split; lia. }
+        eapply progress_inside_supplies; eauto.
+        eapply job_nonpreemptive_after_run_to_completion_threshold; eauto 2.
+        - rewrite -(leqRW H_enough_service).
+          by apply H_valid_run_to_completion_threshold.
+        - move: H_job_j_is_not_completed; apply contra.
+          by apply completion_monotonic; lia.
+      Qed.
+
+  End AuxiliaryLemmas.
+
+  (** For clarity, let's define a local name for the search space. *)
+  Let is_in_search_space_rs := is_in_search_space L IBF_P.
+
+  (** We use the following equation to bound the response-time of a
+      job of task [tsk]. Consider any value [R] that upper-bounds the
+      solution of each response-time recurrence, i.e., for any
+      relative arrival time [A] in the search space, there exists a
+      corresponding solution [F] such that (1) [F <= A + R],
+      (2) [task_rtct tsk + intra_IBF tsk A F <= SBF F] and [SBF F +
+      (task_cost tsk - task_rtct tsk) <= SBF (A + R)].
+
+      Note that, compared to "ideal RTA," there is an additional requirement
+      [F <= A + R]. Intuitively, it is needed to rule out a nonsensical
+      situation when the non-preemptive stage completes earlier than
+      the preemptive stage.  *)
+  Variable R : duration.
+  Hypothesis H_R_is_maximum_rs :
+    forall (A : duration),
+      is_in_search_space_rs A ->
+      exists (F : duration),
+        F <= A + R
+        /\ task_rtct tsk + intra_IBF A F <= SBF F
+        /\ SBF F + (task_cost tsk - task_rtct tsk) <= SBF (A + R).
+
+  (** In the following section we prove that all the premises of
+      abstract RTA are satisfied. *)
+  Section RSaRTAPremises.
+
+    (** First, we show that [IBF_P] correctly upper-bounds
+        interference in the preemptive stage of execution. *)
+    Lemma IBF_P_bounds_interference :
+      job_interference_is_bounded_by
+        arr_seq sched tsk IBF_P (relative_arrival_time_of_job_is_A sched).
+    Proof.
+      move=> t1 t2 Δ j ARR TSK BUSY LT NCOM A PAR; move: (PAR _ _ BUSY) => EQ.
+      rewrite fold_cumul_interference.
+      rewrite (leqRW (cumulative_job_interference_bound _ _ _ _ _ t2 _ _ _ _)) => //.
+      - rewrite leq_add2l /cumul_intra_interference.
+        by apply: H_intra_supply_interference_is_bounded => //.
+      - by eapply incomplete_implies_positive_cost => //.
+      - by apply BUSY.
+    Qed.
+
+    (** Next, we prove that [IBF_NP] correctly bounds interference in
+        the non-preemptive stage given a solution to the preemptive
+        stage [F]. *)
+    Lemma IBF_NP_bounds_interference :
+      job_interference_is_bounded_by
+        arr_seq sched tsk IBF_NP (relative_time_to_reach_rtct sched tsk IBF_P).
+    Proof.
+      have USER : unit_service_proc_model PState by apply unit_supply_is_unit_service.
+      move=> t1 t2 Δ j ARR TSK BUSY LT NCOM F RT.
+      have POS := incomplete_implies_positive_cost _ _ _ NCOM.
+      move: (RT _ _ BUSY) (BUSY) => [FIX RTC] [[/andP [LE1 LE2] _] _].
+      have RleF : task_rtct tsk <= F.
+      { apply cumulative_service_ge_delta with (j := j) (t := t1) (sched := sched) => //.
+        rewrite -[X in _ <= X]add0n.
+        by erewrite <-cumulative_service_before_job_arrival_zero;
+          first erewrite service_during_cat with (t1 := 0) => //; auto; lia. }
+      rewrite /IBF_NP addnBAC // leq_subRL_impl // addnC.
+      have [NEQ1|NEQ1] := leqP t2 (t1 + F); last have [NEQ2|NEQ2] := leqP F Δ.
+      { rewrite -leq_subLR in NEQ1.
+        rewrite -{1}(leqRW NEQ1) (leqRW RTC) (leqRW (service_at_most_cost _ _ _ _ _)) => //.
+        rewrite (leqRW (cumulative_interference_sub _ _ _ _ t1 t2 _ _)) => //.
+        rewrite (leqRW (service_within_busy_interval_ge_job_cost _ _ _ _ _ _ _)) => //.
+        have LLL : (t1 < t2) by lia.
+        interval_to_duration t1 t2 k.
+        by rewrite addnC (leqRW (service_and_interference_bound _ _ _ _ _ _ _ _ _ _ _ _)) => //; lia. }
+      { rewrite addnC -{1}(leqRW FIX) -addnA leq_add2l /IBF_P.
+        rewrite (@addnC (_ - _) _) -addnA subnKC; last by apply complement_SBF_monotone.
+        rewrite -/(cumulative_interference _ _ _).
+        erewrite <-blackout_plus_local_is_interference_cumul with (t2 := t2) => //; last by apply BUSY. 
+        rewrite addnC leq_add //; last first.
+        { by eapply blackout_during_bound with (t2 := t2) => //; split; [ | apply BUSY]. }
+        rewrite /cumul_intra_interference (cumulative_interference_cat _ j (t1 + F)) //=; last by lia.
+        rewrite -!/(cumul_intra_interference _ _ _ _).
+        rewrite (no_intra_interference_after_F _ _ _ _ _ t2) //; last by move: BUSY => [].
+        rewrite addn0 //; eapply H_intra_supply_interference_is_bounded => //.
+        - by move : NCOM; apply contra, completion_monotonic; lia.
+        - move => t1' t2' BUSY'.
+          have [EQ1 E2] := busy_interval_is_unique _ _ _ _ _ _ BUSY BUSY'.
+          by subst; lia. }
+      { rewrite addnC (leqRW RTC); eapply leq_trans.
+        - by erewrite leq_add2l; apply cumulative_interference_sub with (bl := t1) (br := t1 + F); lia.
+        - erewrite no_service_before_busy_interval => //.
+          by rewrite (leqRW (service_and_interference_bound _ _ _ _ _ _ _ _ _ _ _ _)) => //; lia.  }
+    Qed.
+
+    (** Next, we prove that [F] is bounded by [task_cost tsk + IBF_NP
+        F Δ] for any [F] and [Δ]. As explained in file
+        [analysis/abstract/abstract_rta], this shows that the second
+        stage indeed takes into account service received in the first
+        stage. *)
+    Lemma IBF_P_sol_le_IBF_NP :
+      forall (F Δ : duration),
+        F <= task_cost tsk + IBF_NP F Δ.
+    Proof.
+      move=> F Δ.
+      have [NEQ|NEQ] := leqP F (task_rtct tsk).
+      - apply: leq_trans; [apply NEQ | ].
+        by apply: leq_trans; [apply H_valid_run_to_completion_threshold | lia].
+      - rewrite addnA (@addnBCA _ F _); try lia.
+        by apply H_valid_run_to_completion_threshold; lia.
+    Qed.
+
+    (** Next we prove that [H_R_is_maximum_rs] implies [H_R_is_maximum]. *)
+    Lemma max_in_rs_hypothesis_impl_max_in_arta_hypothesis :
+      forall (A : duration),
+        is_in_search_space L IBF_P A ->
+        exists (F : duration),
+          task_rtct tsk + (F - SBF F + intra_IBF A F) <= F
+          /\ task_cost tsk + (F - task_rtct tsk + (A + R - SBF (A + R) - (F - SBF F))) <= A + R.
+    Proof.
+      move=> A SP.
+      case: (H_R_is_maximum_rs A SP) => [F [EQ0 [EQ1 EQ2]]].
+      exists F; split.
+      { have -> : forall a b c, a + (b + c) = (a + c) + b by lia.
+        have -T : forall a b c, c >= b -> (a <= c - b) -> (a + b <= c); [by lia | apply: T; first by lia].
+        have LE : SBF F <= F by eapply sbf_bounded_by_duration; eauto.
+        by rewrite (leqRW EQ1); lia.
+      }
+      { have JJ := IBF_P_sol_le_IBF_NP F (A + R); rewrite /IBF_NP in JJ.
+        rewrite addnA; rewrite addnA in JJ.
+        have T: forall a b c, c >= b -> (a <= c - b) -> (a + b <= c); [by lia | apply: T; first by lia].
+        rewrite subnA; [ | by apply complement_SBF_monotone | by lia].
+        have LE : forall Δ, SBF Δ <= Δ by move => ?; eapply sbf_bounded_by_duration; eauto.
+        rewrite subKn; last by eauto.
+        have T: forall a b c d e, b >= e -> b >= c ->  e + (a - c) <= d -> a + (b - c) <= d + (b - e) by lia.
+        apply : T => //.
+        eapply leq_trans; last by apply LE.
+        by rewrite -(leqRW EQ1); lia.
+      }
+    Qed.
+
+  End RSaRTAPremises.
+
+  (** Finally, we apply the [uniprocessor_response_time_bound]
+      theorem, and using the lemmas above, we prove that all the
+      requirements are satisfied. So, [R] is a response time bound. *)
+  Theorem uniprocessor_response_time_bound_restricted_supply :
+    task_response_time_bound arr_seq sched tsk R.
+  Proof.
+    eapply uniprocessor_response_time_bound => //.
+    { by apply IBF_P_bounds_interference. }
+    { by apply IBF_NP_bounds_interference. }
+    { by apply IBF_P_sol_le_IBF_NP. }
+    { by apply max_in_rs_hypothesis_impl_max_in_arta_hypothesis. }
+  Qed.
+
+End AbstractRTARestrictedSupply.

analysis/abstract/restricted_supply/abstract_seq_rta.v

+Require Export prosa.analysis.facts.model.rbf.
+Require Export prosa.analysis.abstract.IBF.supply_task.
+Require Export prosa.analysis.abstract.restricted_supply.abstract_rta.
+
+(** * Abstract Response-Time Analysis for Restricted-Supply Processors with Sequential Tasks *)
+(** In this section we propose a general framework for response-time
+    analysis (RTA) for real-time tasks with arbitrary arrival models
+    and _sequential_ _tasks_ under uni-processor scheduling subject to
+    supply restrictions, characterized by a given [SBF]. *)
+
+(** In this section, we assume tasks to be sequential. This allows us
+    to establish a more precise response-time bound, since jobs of the
+    same task will be executed strictly in the order they arrive. *)
+Section AbstractRTARestrictedSupplySequential.
+
+  (** Consider any type of tasks ... *)
+  Context {Task : TaskType}.
+  Context `{TaskCost Task}.
+  Context `{TaskRunToCompletionThreshold Task}.
+
+  (**  ... and any type of jobs associated with these tasks. *)
+  Context {Job : JobType}.
+  Context `{JobTask Job Task}.
+  Context `{JobArrival Job}.
+  Context {jc : JobCost Job}.
+  Context `{JobPreemptable Job}.
+
+  (** Consider any kind of fully-supply-consuming, unit-supply
+      processor state model. *)
+  Context `{PState : ProcessorState Job}.
+  Hypothesis H_uniprocessor_proc_model : uniprocessor_model PState.
+  Hypothesis H_unit_supply_proc_model : unit_supply_proc_model PState.
+  Hypothesis H_consumed_supply_proc_model : fully_consuming_proc_model PState.
+
+  (** Consider any valid arrival sequence. *)
+  Variable arr_seq : arrival_sequence Job.
+  Hypothesis H_valid_arrivals : valid_arrival_sequence arr_seq.
+
+  (** Consider any restricted supply uniprocessor schedule of this
+      arrival sequence ... *)
+  Variable sched : schedule PState.
+  Hypothesis H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched arr_seq.
+
+  (** ... where jobs do not execute before their arrival nor after completion. *)
+  Hypothesis H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched.
+  Hypothesis H_completed_jobs_dont_execute : completed_jobs_dont_execute sched.
+
+  (** Assume that the job costs are no larger than the task costs. *)
+  Hypothesis H_valid_job_cost :
+    arrivals_have_valid_job_costs arr_seq.
+
+  (** Consider a task set [ts] ... *)
+  Variable ts : list Task.
+
+  (** ... and a task [tsk] of [ts] that is to be analyzed. *)
+  Variable tsk : Task.
+  Hypothesis H_tsk_in_ts : tsk \in ts.
+
+  (** Consider a valid preemption model ... *)
+  Hypothesis H_valid_preemption_model : valid_preemption_model arr_seq sched.
+
+  (** ... with valid task run-to-completion thresholds. That is,
+      [task_rtc tsk] is (1) no bigger than [tsk]'s cost and (2) for
+      any job [j] of task [tsk] [job_rtct j] is bounded by [task_rtct
+      tsk]. *)
+  Hypothesis H_valid_run_to_completion_threshold :
+    valid_task_run_to_completion_threshold arr_seq tsk.
+
+  (** 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.
+  Hypothesis H_is_arrival_curve : taskset_respects_max_arrivals arr_seq ts.
+
+  (** Assume we are provided with functions characterizing
+      interference and interfering workload. *)
+  Context `{Interference Job}.
+  Context `{InterferingWorkload Job}.
+
+  (** Let's define a local name for clarity. *)
+  Let task_rbf := task_request_bound_function tsk.
+
+  (** We assume that the scheduler is work-conserving. *)
+  Hypothesis H_work_conserving : work_conserving arr_seq sched.
+
+  (** Unlike the more general, underlying theorem
+      [uniprocessor_response_time_bound_restricted_supply], we assume
+      that tasks are sequential. *)
+  Hypothesis H_sequential_tasks : sequential_tasks arr_seq sched.
+  Hypothesis H_interference_and_workload_consistent_with_sequential_tasks :
+    interference_and_workload_consistent_with_sequential_tasks arr_seq sched tsk.
+
+  (** Let [L] be a constant that bounds any busy interval of task [tsk]. *)
+  Variable L : duration.
+  Hypothesis H_busy_interval_exists :
+    busy_intervals_are_bounded_by arr_seq sched tsk L.
+
+  (** Consider a unit SBF valid in busy intervals (w.r.t. task
+      [tsk]). That is, (1) [SBF 0 = 0], (2) for any duration [Δ], the
+      supply produced during a busy-interval prefix of length [Δ] is
+      at least [SBF Δ], and (3) [SBF] makes steps of at most one. *)
+  Context {SBF : SupplyBoundFunction}.
+  Hypothesis H_valid_SBF : valid_busy_sbf arr_seq sched tsk SBF.
+  Hypothesis H_unit_SBF : unit_supply_bound_function SBF.
+
+  (** Next, we assume that [task_intra_IBF] is a bound on intra-supply
+      interference incurred by task [tsk]. That is, [task_intra_IBF]
+      bounds interference ignoring interference due to lack of supply
+      _and_ due to self-interference. *)
+  Variable task_intra_IBF : duration -> duration -> duration.
+  Hypothesis H_interference_inside_reservation_is_bounded :
+    task_intra_interference_is_bounded_by arr_seq sched tsk task_intra_IBF.
+
+  (** We use the function [task_intra_IBF], which satisfies the
+      hypothesis [task_intra_interference_is_bounded_by], to construct
+      a new function [intra_IBF := (task_rbf (A + ε) - task_cost tsk)
+      + task_intra_IBF A Δ] that satisfies the hypothesis
+      [intra_interference_is_bounded_by]. This is needed to later
+      apply the lemma
+      [uniprocessor_response_time_bound_restricted_supply] from file
+      [restricted_supply/abstract_rta] (recall that it requires
+      [intra_IBF], not [task_intra_IBF]). *)
+
+  (** The logic behind [intra_IBF] is quite simple. Consider a job [j]
+      of task [tsk] that arrives exactly [A] units after the beginning
+      of the busy interval. Then the bound on the total interference
+      incurred by [j] within an interval of length [Δ] is no greater
+      than [task_rbf (A + ε) - task_cost tsk + task_intra_IBF A
+      Δ]. Note that, for sequential tasks, the bound consists of two
+      parts: (1) the part that bounds the interference received from
+      other jobs of task [tsk] -- [task_rbf (A + ε) - task_cost tsk]
+      -- and (2) any other interference that is bounded by
+      [task_intra_IBF(tsk, A, Δ)]. *)
+  Let intra_IBF (A Δ : duration) :=
+    (task_rbf (A + ε) - task_cost tsk) + task_intra_IBF A Δ.
+
+  (** For clarity, let's define a local name for the search space. *)
+  Let is_in_search_space_rs := is_in_search_space L intra_IBF.
+
+  (** We use the following equation to bound the response-time of a
+      job of task [tsk]. Consider any value [R] that upper-bounds the
+      solution of each response-time recurrence, i.e., for any
+      relative arrival time [A] in the search space, there exists a
+      corresponding solution [F] such that
+      (1) [F <= A + R],
+      (2) [(task_rbf (A + ε) - (task_cost tsk - task_rtct tsk)) + task_intra_IBF A F <= SBF F],
+      (3) and [SBF F + (task_cost tsk - task_rtct tsk) <= SBF (A + R)]. *)
+  Variable R : duration.
+  Hypothesis H_R_is_maximum_seq_rs :
+    forall (A : duration),
+      is_in_search_space_rs A ->
+      exists (F : duration),
+        F <= A + R
+        /\ (task_rbf (A + ε) - (task_cost tsk - task_rtct tsk)) + task_intra_IBF A F <= SBF F
+        /\ SBF F + (task_cost tsk - task_rtct tsk) <= SBF (A + R).
+
+  (** In the following section we prove that all the premises of
+      [aRSA] are satisfied. *)
+  Section aRSAPremises.
+
+    (** First, we show that [intra_IBF] correctly upper-bounds
+        interference in the preemptive stage of execution. *)
+    Lemma IBF_P_bounds_interference :
+      intra_interference_is_bounded_by arr_seq sched tsk intra_IBF.
+    Proof.
+      move=> t1 t2 Δ j ARR TSK BUSY LT NCOM A PAR; move: (PAR _ _ BUSY) => EQ.
+      have [ZERO|POS] := posnP (@job_cost _ jc j).
+      { exfalso; move: NCOM => /negP NCOM; apply: NCOM.
+        by rewrite /service.completed_by ZERO. }
+      rewrite (cumul_cond_interference_ID _ (nonself arr_seq sched)).
+      rewrite /intra_IBF addnC leq_add; first by done.
+      { rewrite -(leq_add2r (cumul_task_interference arr_seq sched j t1 (t1 + Δ))).
+        eapply leq_trans; first last.
+        { by rewrite EQ; apply: task.cumulative_job_interference_bound => //. }
+        { rewrite -big_split //= leq_sum // /cond_interference  => t _.
+          by case (interference j t), (has_supply sched t), (nonself arr_seq sched j t) => //. } }
+      { rewrite (cumul_cond_interference_pred_eq _ (nonself_intra arr_seq sched)) => //.
+        by move=> s t; split=> //; rewrite andbC. }
+    Qed.
+
+    (** To rule out pathological cases with the
+        [H_R_is_maximum_seq_rs] equation (such as [task_cost tsk]
+        being greater than [task_rbf (A + ε)]), we assume that the
+        arrival curve is non-pathological. *)
+    Hypothesis H_arrival_curve_pos : 0 < max_arrivals tsk ε.
+
+    (** To later apply the theorem
+        [uniprocessor_response_time_bound_restricted_supply], we need
+        to provide the IBF, which bounds the total interference. *)
+    Let IBF A Δ := Δ - SBF Δ + intra_IBF A Δ.
+
+    (** Next we prove that [H_R_is_maximum_seq_rs] implies
+        [H_R_is_maximum_rs] from file ([.../restricted_supply/abstract_rta.v]).
+        In other words, a solution to the response-time recurrence for
+        restricted-supply processor models with sequential tasks can
+        be translated to a solution for the same processor model with
+        non-necessarily sequential tasks. *)
+    Lemma sol_seq_rs_equation_impl_sol_rs_equation :
+      forall (A : duration),
+        is_in_search_space L IBF  A ->
+        exists F : duration,
+          F <= A + R
+          /\ task_rtct tsk + intra_IBF A F <= SBF F
+          /\ SBF F + (task_cost tsk - task_rtct tsk) <= SBF (A + R).
+    Proof.
+      rewrite /IBF; move=> A SP.
+      move: (H_R_is_maximum_seq_rs A) => T.
+      feed T.
+      { move: SP => [ZERO|[POS [x [LT NEQ]]]]; first by left.
+        by right; split => //; exists x; split => //. }
+      have [F [EQ0 [EQ1 EQ2]]] := T; clear T.
+      exists F; split => //; split => //.
+      rewrite /intra_IBF -(leqRW EQ1) addnA leq_add2r.
+      rewrite addnBA; last first.
+      { apply leq_trans with (task_rbf 1).
+        - by apply: task_rbf_1_ge_task_cost => //.
+        - by eapply task_rbf_monotone => //; rewrite addn1. }
+      { rewrite subnBA.
+        - by rewrite addnC.
+        - by apply H_valid_run_to_completion_threshold. }
+    Qed.
+
+  End aRSAPremises.
+
+  (** Finally, we apply the
+      [uniprocessor_response_time_bound_restricted_supply] theorem,
+      and using the lemmas above, prove that all its requirements are
+      satisfied. Hence, [R] is a response-time bound for task [tsk]. *)
+  Theorem uniprocessor_response_time_bound_restricted_supply_seq :
+    task_response_time_bound arr_seq sched tsk R.
+  Proof.
+    move => j ARR TSK.
+    eapply uniprocessor_response_time_bound_restricted_supply => //.
+    { exact: IBF_P_bounds_interference. }
+    { exact: sol_seq_rs_equation_impl_sol_rs_equation. }
+  Qed.
+
+End AbstractRTARestrictedSupplySequential.

analysis/abstract/restricted_supply/bounded_bi/aux.v

+Require Export prosa.analysis.abstract.restricted_supply.iw_instantiation.
+
+
+(** * Helper Lemmas for Bounded Busy Interval Lemmas *)
+
+(** In this section, we introduce a few lemmas that facilitate the
+    proof of an upper bound on busy intervals for various priority
+    policies in the context of the restricted-supply processor
+    model. *)
+Section BoundedBusyIntervalsAux.
+
+  (** 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 any kind of fully supply-consuming unit-supply
+      uniprocessor model. *)
+  Context `{PState : ProcessorState Job}.
+  Hypothesis H_uniprocessor_proc_model : uniprocessor_model PState.
+  Hypothesis H_unit_supply_proc_model : unit_supply_proc_model PState.
+  Hypothesis H_consumed_supply_proc_model : fully_consuming_proc_model PState.
+
+  (** Consider a JLFP policy that indicates a higher-or-equal
+      priority relation, and assume that the relation is reflexive. *)
+  Context {JLFP : JLFP_policy Job}.
+  Hypothesis H_priority_is_reflexive : reflexive_job_priorities JLFP.
+
+  (** Consider any valid arrival sequence. *)
+  Variable arr_seq : arrival_sequence Job.
+  Hypothesis H_valid_arrival_sequence : valid_arrival_sequence arr_seq.
+
+  (** Next, consider a schedule of this arrival sequence, ... *)
+  Variable sched : schedule PState.
+
+  (** ... allow for any work-bearing notion of job readiness, ... *)
+  Context `{!JobReady Job PState}.
+  Hypothesis H_job_ready : work_bearing_readiness arr_seq sched.
+
+  (** ... and assume that the schedule is valid. *)
+  Hypothesis H_sched_valid : valid_schedule sched arr_seq.
+
+  (** Recall that [busy_intervals_are_bounded_by] is an abstract
+      notion. Hence, we need to introduce interference and interfering
+      workload. We will use the restricted-supply instantiations. *)
+
+  (** We say that job [j] incurs interference at time [t] iff it
+      cannot execute due to (1) the lack of supply at time [t], (2)
+      service inversion (i.e., a lower-priority job receiving service
+      at [t]), or a higher-or-equal-priority job receiving service. *)
+  #[local] Instance rs_jlfp_interference : Interference Job :=
+    rs_jlfp_interference arr_seq sched.
+
+  (** The interfering workload, in turn, is defined as the sum of the
+      blackout predicate, service inversion predicate, and the
+      interfering workload of jobs with higher or equal priority. *)
+  #[local] Instance rs_jlfp_interfering_workload : InterferingWorkload Job :=
+    rs_jlfp_interfering_workload arr_seq sched.
+
+  (** Assume that the schedule is work-conserving in the abstract sense. *)
+  Hypothesis H_work_conserving : abstract.definitions.work_conserving arr_seq sched.
+
+  (** Consider any job [j] of task [tsk] that has a positive job cost
+      and is in the arrival sequence. *)
+  Variable j : Job.
+  Hypothesis H_j_arrives : arrives_in arr_seq j.
+  Hypothesis H_job_cost_positive : job_cost_positive j.
+
+  (** First, we note that, since job [j] is pending at time
+      [job_arrival j], there is a (potentially unbounded) busy
+      interval that starts no later than with the arrival of [j]. *)
+  Lemma busy_interval_prefix_exists :
+    exists t1,
+      t1 <= job_arrival j
+      /\ busy_interval_prefix arr_seq sched j t1 (job_arrival j).+1.
+  Proof.
+    have PEND : pending sched j (job_arrival j) by apply job_pending_at_arrival => //.
+    have PREFIX := busy_interval.exists_busy_interval_prefix ltac:(eauto) j.
+    feed (PREFIX (job_arrival j)); first by done.
+    move: PREFIX => [t1 [PREFIX /andP [GE1 _]]].
+    by eexists; split; last by apply instantiated_busy_interval_prefix_equivalent_busy_interval_prefix => //.
+  Qed.
+
+  (** Let <[t1, t2)>> be a busy-interval prefix. *)
+  Variable t1 t2 : instant.
+  Hypothesis H_busy_prefix : busy_interval_prefix arr_seq sched j t1 t2.
+
+  (** We show that the service of higher-or-equal-priority jobs is
+      less than the workload of higher-or-equal-priority jobs in any
+      subinterval <<[t1, t)>> of the interval <<[t1, t2)>>. *)
+  Lemma service_lt_workload_in_busy :
+    forall t,
+      t1 < t < t2 ->
+      service_of_hep_jobs arr_seq sched j t1 t
+      < workload_of_hep_jobs arr_seq j t1 t.
+  Proof.
+    move=> t /andP [LT1 LT2]; move: (H_busy_prefix) => PREF.
+    move_neq_up LE.
+    have EQ: workload_of_hep_jobs arr_seq j t1 t = service_of_hep_jobs arr_seq sched j t1 t.
+    { apply/eqP; rewrite eqn_leq; apply/andP; split => //.
+      by apply service_of_jobs_le_workload => //.
+    }
+    clear LE; move: PREF => [LT [QT1 [NQT QT2]]].
+    specialize (NQT t ltac:(lia)); apply: NQT => s ARR HEP BF.
+    have EQ2: workload_of_hep_jobs arr_seq j 0 t = service_of_hep_jobs arr_seq sched j 0 t.
+    { rewrite /workload_of_hep_jobs (workload_of_jobs_cat _ t1); last by lia.
+      rewrite /service_of_hep_jobs (service_of_jobs_cat_scheduling_interval _ _ _ _ _ 0 t t1) //; last by lia.
+      rewrite /workload_of_hep_jobs in EQ; rewrite EQ; clear EQ.
+      apply/eqP; rewrite eqn_add2r.
+      replace (service_of_jobs sched (hep_job^~ j) (arrivals_between arr_seq 0 t1) t1 t) with 0; last first.
+      { symmetry; apply: big1_seq => h /andP [HEPh BWh].
+        apply big1_seq => t' /andP [_ IN].
+        apply not_scheduled_implies_no_service, completed_implies_not_scheduled => //.
+        apply: completion_monotonic; last apply QT1 => //.
+        { by rewrite mem_index_iota in IN; lia. }
+        { by apply: in_arrivals_implies_arrived. }
+        { by apply: in_arrivals_implies_arrived_before. }
+      }
+      rewrite addn0; apply/eqP.
+      apply all_jobs_have_completed_impl_workload_eq_service => //.
+      move => h ARRh HEPh; apply: QT1 => //.
+      - by apply: in_arrivals_implies_arrived.
+      - by apply: in_arrivals_implies_arrived_before.
+    }
+    by apply: workload_eq_service_impl_all_jobs_have_completed => //.
+  Qed.
+
+  (** Consider a subinterval <<[t1, t1 + Δ)>> of the interval <<[t1,
+      t2)>>. We show that the sum of [j]'s workload and the cumulative
+      workload in <<[t1, t1 + Δ)>> is strictly larger than [Δ]. *)
+  Lemma workload_exceeds_interval :
+    forall Δ,
+      0 < Δ ->
+      t1 + Δ < t2 ->
+      Δ < workload_of_job arr_seq j t1 (t1 + Δ) + cumulative_interfering_workload j t1 (t1 + Δ).
+  Proof.
+    move=> δ POS LE; move: (H_busy_prefix) => PREF.
+    apply leq_ltn_trans with (service_during sched j t1 (t1 + δ) + cumulative_interference j t1 (t1 + δ)).
+    { rewrite /service_during /cumulative_interference /cumul_cond_interference  /cond_interference /service_at.
+      rewrite -big_split //= -{1}(sum_of_ones t1 δ) big_nat [in X in _ <= X]big_nat.
+      apply leq_sum => x /andP[Lo Hi].
+      { move: (H_work_conserving j t1 t2 x) => Workj.
+        feed_n 4 Workj; try done.
+        { by apply instantiated_busy_interval_prefix_equivalent_busy_interval_prefix. }
+        { by apply/andP; split; eapply leq_trans; eauto. }
+        destruct interference.
+        - by lia.
+        - by rewrite //= addn0; apply Workj.
+      }
+    }
+    rewrite cumulative_interfering_workload_split // cumulative_interference_split //.
+    rewrite cumulative_iw_hep_eq_workload_of_ohep cumulative_i_ohep_eq_service_of_ohep //; last by apply PREF.
+    rewrite -[leqRHS]addnC -[leqRHS]addnA [(_ + workload_of_job _ _ _ _)]addnC.
+    rewrite workload_job_and_ahep_eq_workload_hep //.
+    rewrite -addnC -addnA [(_ + service_during _ _ _ _ )]addnC.
+    rewrite service_plus_ahep_eq_service_hep //; last by move: PREF => [_ [_ [_ /andP [A B]]]].
+    rewrite ltn_add2l.
+    by apply: service_lt_workload_in_busy; eauto; lia.
+  Qed.
+
+End BoundedBusyIntervalsAux.

analysis/abstract/restricted_supply/bounded_bi/edf.v

+Require Export prosa.model.priority.edf.
+Require Export prosa.model.task.absolute_deadline.
+Require Export prosa.analysis.definitions.busy_interval.edf_pi_bound.
+Require Export prosa.analysis.abstract.restricted_supply.abstract_rta.
+Require Export prosa.analysis.abstract.restricted_supply.bounded_bi.aux.
+Require Export prosa.analysis.definitions.sbf.busy.
+
+(** * Sufficient Condition for Bounded Busy Intervals for RS EDF *)
+
+(** In this section, we show that the existence of [L] such that
+    [total_rbf L <= SBF L /\ longest_busy_interval_with_pi <= SBF L],
+    where [longest_busy_interval_with_pi] is the length of the longest
+    busy interval starting with a priority inversion (w.r.t. a job of
+    a task under analysis) and [SBF] is a supply-bound function, is a
+    sufficient condition for the existence of bounded busy intervals
+    under EDF scheduling with a restricted-supply processor model.
+
+    The proof uses the following observation. Consider the beginning
+    of a busy interval of a job [j] to be analyzed. If there is
+    service inversion, one can derive an upper bound on the relative
+    arrival of job [j], which in turn can be used to derive a bound on
+    the total higher-or-equal priority workload
+    ([longest_busy_interval_with_pi]). If there is no service
+    inversion, we use the standard fixpoint approach with [total_rbf L]. *)
+Section BoundedBusyIntervals.
+
+  (** Consider any type of tasks ... *)
+  Context {Task : TaskType}.
+  Context `{TaskCost Task}.
+  Context `{TaskDeadline Task}.
+
+  (**  ... and any type of jobs associated with these tasks. *)
+  Context {Job : JobType}.
+  Context `{JobTask Job Task}.
+  Context `{JobArrival Job}.
+  Context `{JobCost Job}.
+
+  (** For brevity, let's denote the relative deadline of a task as [D]. *)
+  Let D tsk := task_deadline tsk.
+
+  (** Consider any kind of fully supply-consuming unit-supply
+      uniprocessor model. *)
+  Context `{PState : ProcessorState Job}.
+  Hypothesis H_uniprocessor_proc_model : uniprocessor_model PState.
+  Hypothesis H_unit_supply_proc_model : unit_supply_proc_model PState.
+  Hypothesis H_consumed_supply_proc_model : fully_consuming_proc_model PState.
+
+  (** Consider any valid arrival sequence. *)
+  Variable arr_seq : arrival_sequence Job.
+  Hypothesis H_valid_arrival_sequence : valid_arrival_sequence arr_seq.
+
+  (** Next, consider a schedule of this arrival sequence, ... *)
+  Variable sched : schedule PState.
+
+  (** ... allow for any work-bearing notion of job readiness, ... *)
+  Context `{!JobReady Job PState}.
+  Hypothesis H_job_ready : work_bearing_readiness arr_seq sched.
+
+  (** ... and assume that the schedule is valid. *)
+  Hypothesis H_sched_valid : valid_schedule sched arr_seq.
+
+  (** Assume that jobs have bounded non-preemptive segments. *)
+  Context `{JobPreemptable Job}.
+  Context `{TaskMaxNonpreemptiveSegment Task}.
+  Hypothesis H_valid_preemption_model : valid_preemption_model arr_seq sched.
+  Hypothesis H_valid_model_with_bounded_nonpreemptive_segments :
+    valid_model_with_bounded_nonpreemptive_segments arr_seq sched.
+
+  (** Furthermore, assume that the schedule respects the scheduling policy. *)
+  Hypothesis H_respects_policy : respects_JLFP_policy_at_preemption_point arr_seq sched (EDF Job).
+
+  (** Recall that [busy_intervals_are_bounded_by] is an abstract
+      notion. Hence, we need to introduce interference and interfering
+      workload. We will use the restricted-supply instantiations. *)
+
+  (** We say that job [j] incurs interference at time [t] iff it
+      cannot execute due to (1) the lack of supply at time [t], (2)
+      service inversion (i.e., a lower-priority job receiving service
+      at [t]), or a higher-or-equal-priority job receiving service. *)
+  #[local] Instance rs_jlfp_interference : Interference Job :=
+    rs_jlfp_interference arr_seq sched.
+
+  (** The interfering workload, in turn, is defined as the sum of the
+      blackout predicate, service inversion predicate, and the
+      interfering workload of jobs with higher or equal priority. *)
+  #[local] Instance rs_jlfp_interfering_workload : InterferingWorkload Job :=
+    rs_jlfp_interfering_workload arr_seq sched.
+
+  (** Assume that the schedule is work-conserving in the abstract sense. *)
+  Hypothesis H_work_conserving : abstract.definitions.work_conserving arr_seq sched.
+
+  (** Consider an arbitrary task set [ts], ... *)
+  Variable ts : seq Task.
+
+  (** ... assume that all jobs come from the task set, ... *)
+  Hypothesis H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts.
+
+  (** ... and that the cost of a job does not exceed its task's WCET. *)
+  Hypothesis H_valid_job_cost : arrivals_have_valid_job_costs arr_seq.
+
+  (** Let [max_arrivals] be a family of valid arrival curves. *)
+  Context `{MaxArrivals Task}.
+  Hypothesis H_valid_arrival_curve : valid_taskset_arrival_curve ts max_arrivals.
+  Hypothesis H_is_arrival_curve : taskset_respects_max_arrivals arr_seq ts.
+
+  (** Let [tsk] be any task in [ts] that is to be analyzed. *)
+  Variable tsk : Task.
+  Hypothesis H_tsk_in_ts : tsk \in ts.
+
+  (** Consider a unit SBF valid in busy intervals (w.r.t. task
+      [tsk]). That is, (1) [SBF 0 = 0], (2) for any duration [Δ], the
+      supply produced during a busy-interval prefix of length [Δ] is
+      at least [SBF Δ], and (3) [SBF] makes steps of at most one. *)
+  Context {SBF : SupplyBoundFunction}.
+  Hypothesis H_valid_SBF : valid_busy_sbf arr_seq sched tsk SBF.
+  Hypothesis H_unit_SBF : unit_supply_bound_function SBF.
+
+  (** First, we show that the constant [longest_busy_interval_with_pi
+      ts tsk] indeed bounds the cumulative interference incurred by
+      job [j]. *)
+  Section LongestBusyIntervalWithPIIsValid.
+
+    (** Consider any job [j] of task [tsk] that has a positive job
+        cost and is in the arrival sequence. *)
+    Variable j : Job.
+    Hypothesis H_j_arrives : arrives_in arr_seq j.
+    Hypothesis H_job_of_tsk : job_of_task tsk j.
+    Hypothesis H_job_cost_positive : job_cost_positive j.
+
+    (** Let <<[t1, t2)>> be a busy-interval prefix. *)
+    Variable t1 t2 : instant.
+    Hypothesis H_busy_prefix : busy_interval_prefix arr_seq sched j t1 t2.
+
+    (** Consider an interval <<[t1, t1 + δ) ⊆ [t1, t2)>>. *)
+    Variable δ : duration.
+    Hypothesis H_interval_in_busy_prefix : t1 + δ <= t2.
+
+    (** Assume that cumulative service inversion of job [j] in this
+        interval is positive. *)
+    Hypothesis H_positive_service_inversion :
+      cumulative_service_inversion arr_seq sched j t1 (t1 + δ) > 0.
+
+    (** The LHS of the following inequality represents all possible
+        interference as well as the cost of the job itself in a prefix
+        of length [δ]. On the RHS of the inequality, there is a
+        constant [longest_busy_interval_with_pi]. We prove that this
+        inequality is indeed true. This implies that if the cumulative
+        service inversion of job [j] is positive, its busy interval
+        cannot possibly be longer than
+        [longest_busy_interval_with_pi]. *)
+    Lemma longest_bi_with_pi_bound_is_valid :
+      cumulative_service_inversion arr_seq sched j t1 (t1 + δ)
+      + (cumulative_other_hep_jobs_interfering_workload arr_seq j t1 (t1 + δ)
+         + workload_of_job arr_seq j t1 (t1 + δ))
+      <= longest_busy_interval_with_pi ts tsk.
+    Proof.
+      move: (H_positive_service_inversion) => PP.
+      eapply cumulative_service_inversion_from_one_job in H_positive_service_inversion => //.
+      move: H_positive_service_inversion => [jlp [ARR [LP EQs]]].
+      move: (H_job_of_tsk) => /eqP TSK; unfold longest_busy_interval_with_pi, D in *; subst tsk.
+      move: (H_busy_prefix) => [_ [_ [_ /andP [ARRj _]]]].
+      have [t_sched [_ SCHEDjlp]]: exists t, t1 <= t < t1 + δ /\ scheduled_at sched jlp t
+          by apply cumulative_service_implies_scheduled; rewrite -EQs.
+      apply leq_bigmax_sup; exists (job_task jlp); split; last split.
+      { by apply H_all_jobs_from_taskset. }
+      {  move_neq_up LP'; move: LP => /negP LP; apply: LP.
+         by rewrite /hep_job /EDF /job_deadline /job_deadline_from_task_deadline; lia. }
+      apply leq_add.
+      - rewrite EQs (leqRW (lp_job_bounded_service _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _)) => //.
+        by rewrite leq_sub2r //; apply H_valid_model_with_bounded_nonpreemptive_segments.
+      - rewrite addnC cumulative_iw_hep_eq_workload_of_ohep workload_job_and_ahep_eq_workload_hep //.
+        apply leq_trans with (workload_of_jobs (hep_job^~ jlp) (arrivals_between arr_seq t1 (t1 + δ))).
+        { apply workload_of_jobs_weaken => jo; move: LP; clear.
+          by rewrite /hep_job /EDF /job_deadline /job_deadline_from_task_deadline; lia. }
+        erewrite workload_of_jobs_partitioned_by_tasks with (ts := undup ts).
+        + eapply leq_trans; first by apply sum_le_subseq, undup_subseq.
+          apply leq_sum_seq => tsk_o INo HEP.
+          set P := (fun j' : Job => hep_job j' jlp && (job_task j' == tsk_o)).
+          rewrite -(leqRW (rbf_spec' _ _ P _ _ _ _ _)) /P //; last by move=> ? /andP[].
+          have [A | B] := (leqP δ (task_deadline (job_task jlp) - task_deadline tsk_o)).
+          { by apply workload_of_jobs_reduce_range; lia. }
+          { have EQt: forall a b, a = b -> a <= b; [by lia | apply: EQt].
+            apply workload_of_jobs_nil_tail => //; [lia | move => jo IN LE].
+            have [EQ|NEQ] := (@eqP _ (job_task jo) (tsk_o)); last by rewrite andbF.
+            rewrite andbT /hep_job /EDF /job_deadline /job_deadline_from_task_deadline -ltnNge.
+            by subst tsk_o; rewrite /hep_job /EDF /job_deadline /job_deadline_from_task_deadline in LP; lia.
+          }
+        + by move=> jo IN; rewrite in_seq_equiv_undup;
+            apply: H_all_jobs_from_taskset; apply: in_arrivals_implies_arrived.
+        + move=> jo IN.
+          have ARRjo : t1 <= job_arrival jo by apply: job_arrival_between_ge.
+          rewrite /hep_job /D /EDF => T; move_neq_up LEQ; move_neq_down T.
+          by rewrite /job_deadline /job_deadline_from_task_deadline; lia.
+        + by apply arrivals_uniq.
+        + by apply undup_uniq.
+    Qed.
+
+  End LongestBusyIntervalWithPIIsValid.
+
+  (** We introduce the main assumption of this section. Let [L]
+      be any positive constant that satisfies two properties. *)
+  Variable L : duration.
+  Hypothesis H_L_positive : L > 0.
+
+  (** First, we assume that [SBF L] bounds
+      [longest_busy_interval_with_pi ts tsk]. As discussed, when a
+      busy interval starts with service inversion, one can upper-bound
+      the total interfering workload that a job under analysis incurs
+      via [longest_busy_interval_with_pi ts tsk]. The time to consume
+      this workload is [SBF L]. *)
+  Hypothesis H_L_bounds_bi_with_pi : longest_busy_interval_with_pi ts tsk <= SBF L.
+
+  (** And second, we assume that [total_RBF L <= SBF L]. When there is
+      no service inversion at the beginning of a busy interval, one
+      can show that there is no carry-in workload (including the
+      lower-priority workload). This allows us to bound interfering
+      workload within a busy interval with [total_RBF L] without
+      adding an extra [+ blocking_bound] as in the case of the general
+      JLFP bound. *)
+  Hypothesis H_fixed_point : total_request_bound_function ts L <= SBF L.
+
+
+  (** In the following, we prove busy-interval boundedness via a case
+      analysis on two cases: (1) when the busy-interval prefix is at
+      least [L] time units long and (2) when the busy interval prefix
+      terminates earlier. In either case, we can show that the
+      busy-interval prefix is bounded. *)
+  Section StepByStepProof.
+
+    (** Consider any job [j] of task [tsk] that has a positive job
+        cost and is in the arrival sequence. *)
+    Variable j : Job.
+    Hypothesis H_j_arrives : arrives_in arr_seq j.
+    Hypothesis H_job_of_tsk : job_of_task tsk j.
+    Hypothesis H_job_cost_positive : job_cost_positive j.
+
+    (** As a preparation step, we show that [L] bounds the relative
+        arrival time of job [j]. *)
+    Section RelativeArrivalIsBounded.
+
+      (** Consider a time instant [t1] such that <<[t1, job_arrival
+          j]>> is a busy-interval prefix of [j]. *)
+      Variable t1 : instant.
+      Hypothesis H_arrives : t1 <= job_arrival j.
+      Hypothesis H_busy_prefix_arr : busy_interval_prefix arr_seq sched j t1 (job_arrival j).+1.
+
+      (** From the properties of the workload (defined by hypotheses
+          [H_L_bounds_bi_with_pi] and [H_fixed_point]), we show that
+          [j]'s arrival time is necessarily less than [t1 + L]. *)
+      Local Lemma job_arrival_is_bounded :
+        job_arrival j < t1 + L.
+      Proof.
+        move_neq_up FF.
+        move: (H_busy_prefix_arr) (H_busy_prefix_arr) => PREFIX PREFIXA.
+        apply instantiated_busy_interval_prefix_equivalent_busy_interval_prefix in PREFIXA => //.
+        move: (PREFIXA) => GTC.
+        eapply workload_exceeds_interval with (Δ := L) in PREFIX => //; last first.
+        move_neq_down PREFIX.
+        rewrite (cumulative_interfering_workload_split _ _ _).
+        rewrite (leqRW (blackout_during_bound _ _ _ _ _ _ _ _ (job_arrival j).+1 _ _ _)); (try apply H_valid_SBF) => //.
+        rewrite addnC -!addnA.
+        have E: forall a b c, a <= c -> b <= c - a -> a + b <= c by move => ? ? ? ? ?; lia.
+        apply: E; first by lia.
+        rewrite subKn; last by apply: sbf_bounded_by_duration => //.
+        have [ZERO|POS] := (posnP (cumulative_service_inversion arr_seq sched j t1 (t1 + L))).
+        { rewrite ZERO add0n -(leqRW H_fixed_point).
+          rewrite addnC cumulative_iw_hep_eq_workload_of_ohep workload_job_and_ahep_eq_workload_hep //.
+          have DD := hep_workload_le_total_rbf.
+          by apply hep_workload_le_total_rbf. }
+        { by rewrite -(leqRW H_L_bounds_bi_with_pi); apply: longest_bi_with_pi_bound_is_valid. }
+      Qed.
+
+    End RelativeArrivalIsBounded.
+
+    (** We start with the first case, where the busy-interval prefix
+        continues until time instant [t1 + L]. *)
+    Section Case1.
+
+      (** Consider a time instant [t1] such that <<[t1, job_arrival
+          j]>> and <<[t1, t1 + L)>> are both busy-interval prefixes of
+          job [j]. *)
+      Variable t1 : instant.
+      Hypothesis H_busy_prefix_arr : busy_interval_prefix arr_seq sched j t1 (job_arrival j).+1.
+      Hypothesis H_busy_prefix_L : busy_interval_prefix arr_seq sched j t1 (t1 + L).
+
+      (** The crucial point to note is that the sum of the job's cost
+          (represented as [workload_of_job]) and the interfering
+          workload in the interval <<[t1, t1 + L)>> is bounded by [L]
+          due to hypotheses [H_L_bounds_bi_with_pi] and
+          [H_fixed_point]. *)
+      Local Lemma workload_is_bounded :
+        workload_of_job arr_seq j t1 (t1 + L) + cumulative_interfering_workload j t1 (t1 + L) <= L.
+      Proof.
+        rewrite (cumulative_interfering_workload_split _ _ _).
+        rewrite (leqRW (blackout_during_bound _ _ _ _ _ _ _ _ (t1 + L) _ _ _)); (try apply H_valid_SBF) => //.
+        rewrite // addnC -!addnA.
+        have E: forall a b c, a <= c -> b <= c - a -> a + b <= c by move => ? ? ? ? ?; lia.
+        apply: E; first by lia.
+        rewrite subKn; last by apply: sbf_bounded_by_duration => //.
+        have [ZERO|POS] := (posnP (cumulative_service_inversion arr_seq sched j t1 (t1 + L))).
+        { rewrite ZERO add0n -(leqRW H_fixed_point).
+          rewrite addnC cumulative_iw_hep_eq_workload_of_ohep workload_job_and_ahep_eq_workload_hep //.
+          by apply hep_workload_le_total_rbf => //; move: (H_busy_prefix_arr) => [LE _]; rewrite -ltnS. }
+        { by rewrite -(leqRW H_L_bounds_bi_with_pi); apply: longest_bi_with_pi_bound_is_valid => //;
+            move: (H_busy_prefix_arr) => [LE _]; rewrite -ltnS. }
+      Qed.
+
+      (** It follows that [t1 + L] is a quiet time, which means that
+          the busy prefix ends (i.e., it is bounded). *)
+      Local Lemma busy_prefix_is_bounded_case1 :
+        exists t2,
+          job_arrival j < t2
+          /\ t2 <= t1 + L
+          /\ busy_interval arr_seq sched j t1 t2.
+      Proof.
+        have PEND : pending sched j (job_arrival j) by apply job_pending_at_arrival => //.
+        enough(exists t2, job_arrival j < t2 /\ t2 <= t1 + L /\ definitions.busy_interval sched j t1 t2) as BUSY.
+        { have [t2 [LE1 [LE2 BUSY2]]] := BUSY.
+          eexists; split; first by exact: LE1.
+          split; first by done.
+          by apply instantiated_busy_interval_equivalent_busy_interval.
+        }
+        eapply busy_interval.busy_interval_is_bounded; eauto 2 => //.
+        - by eapply instantiated_i_and_w_no_speculative_execution; eauto 2 => //.
+        - by apply instantiated_busy_interval_prefix_equivalent_busy_interval_prefix => //.
+        - by apply workload_is_bounded => //.
+      Qed.
+
+    End Case1.
+
+    (** Next, we consider the case when the interval <<[t1, t1 + L)>>
+        is not a busy-interval prefix. *)
+    Section Case2.
+
+      (** Consider a time instant [t1] such that <<[t1, job_arrival
+          j]>> is a busy-interval prefix of [j] and <<[t1, t1 + L)>>
+          is _not_. *)
+      Variable t1 : instant.
+      Hypothesis H_arrives : t1 <= job_arrival j.
+      Hypothesis H_busy_prefix_arr : busy_interval_prefix arr_seq sched j t1 (job_arrival j).+1.
+      Hypothesis H_no_busy_prefix_L : ~ busy_interval_prefix arr_seq sched j t1 (t1 + L).
+
+      (** Lemma [job_arrival_is_bounded] implies that the
+          busy-interval prefix starts at time [t1], continues until
+          [job_arrival j + 1], and then terminates before [t1 + L].
+          Or, in other words, there is point in time [t2] such that
+          (1) [j]'s arrival is bounded by [t2], (2) [t2] is bounded by
+          [t1 + L], and (3) <<[t1, t2)>> is busy interval of job
+          [j]. *)
+      Local Lemma busy_prefix_is_bounded_case2:
+        exists t2,
+          job_arrival j < t2
+          /\ t2 <= t1 + L
+          /\ busy_interval arr_seq sched j t1 t2.
+      Proof.
+        have LE: job_arrival j < t1 + L
+          by apply job_arrival_is_bounded => //; try apply instantiated_busy_interval_prefix_equivalent_busy_interval_prefix.
+        move: (H_busy_prefix_arr) => PREFIX.
+        move: (H_no_busy_prefix_L) => NOPREF.
+        apply instantiated_busy_interval_prefix_equivalent_busy_interval_prefix in PREFIX => //.
+        have BUSY := terminating_busy_prefix_is_busy_interval _ _ _ _ _ _ _ PREFIX.
+        edestruct BUSY as [t2 BUS]; clear BUSY; try apply TSK; eauto 2 => //.
+        { move => T; apply: NOPREF.
+          by apply instantiated_busy_interval_prefix_equivalent_busy_interval_prefix in T => //.
+        }
+        exists t2; split; last split.
+        { move: BUS => [[A _] _]; lia. }
+        { move_neq_up FA.
+          apply: NOPREF; split; [lia | split; first by apply H_busy_prefix_arr].
+          split.
+          - move=> t NEQ.
+            apply abstract_busy_interval_classic_busy_interval_prefix in BUS => //.
+            by apply BUS; lia.
+          - lia.
+        }
+        { by apply instantiated_busy_interval_equivalent_busy_interval => //. }
+      Qed.
+
+    End Case2.
+
+  End StepByStepProof.
+
+  (** Combining the cases analyzed above, we conclude that busy
+      intervals of jobs released by task [tsk] are bounded by [L].  *)
+  Lemma busy_intervals_are_bounded_rs_edf :
+    busy_intervals_are_bounded_by arr_seq sched tsk L.
+  Proof.
+    move => j ARR TSK POS.
+    have PEND : pending sched j (job_arrival j) by apply job_pending_at_arrival => //.
+    edestruct ( busy_interval_prefix_exists) as [t1 [GE PREFIX]]; eauto 2; first by apply EDF_is_reflexive.
+    exists t1.
+    enough(exists t2, job_arrival j < t2 /\ t2 <= t1 + L /\ busy_interval arr_seq sched j t1 t2) as BUSY.
+    { move: BUSY => [t2 [LT [LE BUSY]]]; eexists; split; last first.
+      { split; first by exact: LE.
+        by apply instantiated_busy_interval_equivalent_busy_interval. }
+      { by apply/andP; split. }
+    }
+    { have [LPREF|NOPREF] := busy_interval_prefix_case ltac:(eauto) j t1 (t1 + L).
+      { apply busy_prefix_is_bounded_case1 => //.
+        by apply instantiated_busy_interval_prefix_equivalent_busy_interval_prefix => //. }
+      { apply busy_prefix_is_bounded_case2=> //.
+        move=> NP; apply: NOPREF.
+        by apply instantiated_busy_interval_prefix_equivalent_busy_interval_prefix => //.
+      }
+    }
+  Qed.
+
+End BoundedBusyIntervals.

analysis/abstract/restricted_supply/bounded_bi/elf.v

+Require Export prosa.analysis.facts.blocking_bound.elf.
+Require Export prosa.analysis.abstract.restricted_supply.abstract_rta.
+Require Export prosa.analysis.abstract.restricted_supply.iw_instantiation.
+Require Export prosa.analysis.abstract.restricted_supply.bounded_bi.aux.
+Require Export prosa.analysis.definitions.sbf.busy.
+Require Export prosa.analysis.facts.priority.jlfp_with_fp.
+
+(** * Sufficient Condition for Bounded Busy Intervals for RS ELF *)
+
+(** In this section, we show that the existence of [L] such that [B +
+    total_hep_rbf L <= SBF L], where [B] is the blocking bound and
+    [SBF] is a supply-bound function, is a sufficient condition for
+    the existence of bounded busy intervals under ELF scheduling with a
+    restricted-supply processor model. *)
+Section BoundedBusyIntervals.
+
+  (** Consider any type of tasks with relative priority-points ... *)
+  Context {Task : TaskType}.
+  Context `{TaskCost Task}.
+  Context `{PriorityPoint Task}.
+
+  (**  ... and any type of jobs associated with these tasks. *)
+  Context {Job : JobType}.
+  Context `{JobTask Job Task}.
+  Context `{JobArrival Job}.
+  Context `{JobCost Job}.
+
+  (** Consider any kind of fully supply-consuming unit-supply
+      uniprocessor model. *)
+  Context `{PState : ProcessorState Job}.
+  Hypothesis H_uniprocessor_proc_model : uniprocessor_model PState.
+  Hypothesis H_unit_supply_proc_model : unit_supply_proc_model PState.
+  Hypothesis H_consumed_supply_proc_model : fully_consuming_proc_model PState.
+
+  (** Consider an FP policy that indicates a higher-or-equal priority
+      relation, and assume that the relation is reflexive, transitive.
+      and total. *)
+  Context (FP : FP_policy Task).
+  Hypothesis H_priority_is_reflexive : reflexive_task_priorities FP.
+  Hypothesis H_priority_is_transitive : transitive_task_priorities FP.
+  Hypothesis H_total_priorities : total_task_priorities FP.
+
+  (** Consider any valid arrival sequence. *)
+  Variable arr_seq : arrival_sequence Job.
+  Hypothesis H_valid_arrival_sequence : valid_arrival_sequence arr_seq.
+
+  (** Next, consider a schedule of this arrival sequence, ... *)
+  Variable sched : schedule PState.
+
+  (** ... allow for any work-bearing notion of job readiness, ... *)
+  Context `{!JobReady Job PState}.
+  Hypothesis H_job_ready : work_bearing_readiness arr_seq sched.
+
+  (** ... and assume that the schedule is valid. *)
+  Hypothesis H_sched_valid : valid_schedule sched arr_seq.
+
+  (** Assume that jobs have bounded non-preemptive segments. *)
+  Context `{JobPreemptable Job}.
+  Context `{TaskMaxNonpreemptiveSegment Task}.
+  Hypothesis H_valid_preemption_model : valid_preemption_model arr_seq sched.
+  Hypothesis H_valid_model_with_bounded_nonpreemptive_segments :
+    valid_model_with_bounded_nonpreemptive_segments arr_seq sched.
+
+  (** Further assume that the schedule follows the ELF scheduling policy. *)
+  Hypothesis H_respects_policy :
+    respects_JLFP_policy_at_preemption_point arr_seq sched (ELF FP).
+
+  (** Recall that [busy_intervals_are_bounded_by] is an abstract
+      notion. Hence, we need to introduce interference and interfering
+      workload. We will use the restricted-supply instantiations. *)
+
+  (** We say that job [j] incurs interference at time [t] iff it
+      cannot execute due to (1) the lack of supply at time [t], (2)
+      service inversion (i.e., a lower-priority job receiving service
+      at [t]), or a higher-or-equal-priority job receiving service. *)
+  #[local] Instance rs_jlfp_interference : Interference Job :=
+    rs_jlfp_interference arr_seq sched.
+
+  (** The interfering workload, in turn, is defined as the sum of the
+      blackout predicate, service inversion predicate, and the
+      interfering workload of jobs with higher or equal priority. *)
+  #[local] Instance rs_jlfp_interfering_workload : InterferingWorkload Job :=
+    rs_jlfp_interfering_workload arr_seq sched.
+
+  (** Assume that the schedule is work-conserving in the abstract sense. *)
+  Hypothesis H_work_conserving : definitions.work_conserving arr_seq sched.
+
+  (** Consider an arbitrary task set [ts], ... *)
+  Variable ts : list Task.
+
+  (** ... assume that all jobs come from the task set, ... *)
+  Hypothesis H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts.
+
+  (** ... and that the cost of a job does not exceed its task's WCET. *)
+  Hypothesis H_valid_job_cost : arrivals_have_valid_job_costs arr_seq.
+
+  (** 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.
+  Hypothesis H_is_arrival_curve : taskset_respects_max_arrivals arr_seq ts.
+
+  (** Let [tsk] be any task in [ts] that is to be analyzed. *)
+  Variable tsk : Task.
+  Hypothesis H_tsk_in_ts : tsk \in ts.
+
+  (** Consider a unit SBF valid in busy intervals (w.r.t. task
+      [tsk]). That is, (1) [SBF 0 = 0], (2) for any duration [Δ], the
+      supply produced during a busy-interval prefix of length [Δ] is
+      at least [SBF Δ], and (3) [SBF] makes steps of at most one. *)
+  Context {SBF : SupplyBoundFunction}.
+  Hypothesis H_valid_SBF : valid_busy_sbf arr_seq sched tsk SBF.
+  Hypothesis H_unit_SBF : unit_supply_bound_function SBF.
+
+  (** The next step is to establish a bound on the maximum busy-window length,
+      which aRSA requires to be given. To this end, let L be any positive
+      fixed point of the busy-interval recurrence. As the lemma
+      busy_intervals_are_bounded_rs_elf shows, under ELF scheduling, this is
+      sufficient to guarantee that all busy intervals are bounded by L. *)
+  Variable L : duration.
+  Hypothesis H_L_positive : 0 < L.
+
+  Hypothesis H_fixed_point:
+    forall (A : duration),
+      blocking_bound ts tsk A + total_hep_request_bound_function_FP ts tsk L <= SBF L.
+
+  (** Next, we provide a step-by-step proof of busy-interval boundedness. *)
+  Section StepByStepProof.
+
+    (** Consider any job [j] of task [tsk] that has a positive job
+        cost and is in the arrival sequence. *)
+    Variable j : Job.
+    Hypothesis H_j_arrives : arrives_in arr_seq j.
+    Hypothesis H_job_of_tsk : job_of_task tsk j.
+    Hypothesis H_job_cost_positive : job_cost_positive j.
+
+    (** Consider [t1] to be the start of the busy-interval. *)
+    Variable t1 : instant.
+
+    (** Now we have two cases: (1) when the busy-interval prefix
+        continues until time instant [t1 + L] and (2) when the busy
+        interval prefix terminates earlier. In either case, we can
+        show that the busy-interval prefix is bounded. *)
+
+    (** We start with the first case, where the busy-interval prefix
+        continues until time instant [t1 + L]. *)
+    Section Case1.
+
+      (** Consider that <<[t1, job_arrival j]>> and <<[t1, t1 + L)>> are both
+          busy-interval prefixes of job [j]. Note that at this point we do not
+          necessarily know that [job_arrival j <= L]; hence, we assume the
+          existence of both prefixes. *)
+      Hypothesis H_busy_prefix_arr : busy_interval_prefix arr_seq sched j t1 (job_arrival j).+1.
+      Hypothesis H_busy_prefix_L : busy_interval_prefix arr_seq sched j t1 (t1 + L).
+
+      (** The crucial point to note is that the sum of the job's cost
+          (represented as [workload_of_job]) and the interfering
+          workload in the interval <<[t1, t1 + L)>> is bounded by [L]
+          due to the fixed point [H_fixed_point]. *)
+      Local Lemma workload_is_bounded :
+        workload_of_job arr_seq j t1 (t1 + L) + cumulative_interfering_workload j t1 (t1 + L) <= L.
+      Proof.
+        rewrite (cumulative_interfering_workload_split _ _ _).
+        rewrite (leqRW (blackout_during_bound _ _ _ _ _ _ _ _ (t1 + L) _ _ _)); (try apply H_valid_SBF) => //.
+        rewrite // addnC -!addnA.
+        have E: forall a b c, a <= c -> b <= c - a -> a + b <= c by move => ? ? ? ? ?; lia.
+        apply: E; first by lia.
+        rewrite subKn; last by apply: sbf_bounded_by_duration => //.
+        specialize (H_fixed_point (job_arrival j - t1)).
+        rewrite -(leqRW H_fixed_point); apply leq_add.
+        - apply: leq_trans; first apply: service_inversion_is_bounded => //.
+          + instantiate (1 := fun (A : duration) => blocking_bound ts tsk A) => //=.
+            by move=> jo t t' ARRo TSKo PREFo; apply: nonpreemptive_segments_bounded_by_blocking => //.
+          + by done.
+        - rewrite addnC cumulative_iw_hep_eq_workload_of_ohep workload_job_and_ahep_eq_workload_hep //.
+          apply workload_of_jobs_bounded => //.
+          move=> j'.
+          move: H_job_of_tsk => /eqP <-.
+          by apply hep_job_implies_hep_task.
+        Qed.
+
+      (** It follows that [t1 + L] is a quiet time, which means that
+          the busy prefix ends (i.e., it is bounded). *)
+      Local Lemma busy_prefix_is_bounded_case1 :
+        exists t2,
+          job_arrival j < t2
+          /\ t2 <= t1 + L
+          /\ busy_interval arr_seq sched j t1 t2.
+      Proof.
+        have PEND : pending sched j (job_arrival j) by apply job_pending_at_arrival => //.
+        enough(exists t2, job_arrival j < t2 /\ t2 <= t1 + L /\ definitions.busy_interval sched j t1 t2) as BUSY.
+        { have [t2 [LE1 [LE2 BUSY2]]] := BUSY.
+          eexists; split; first by exact: LE1.
+          split; first by done.
+          by apply instantiated_busy_interval_equivalent_busy_interval.
+        }
+        eapply busy_interval.busy_interval_is_bounded; eauto 2 => //.
+        - by eapply instantiated_i_and_w_no_speculative_execution; eauto 2 => //.
+        - by apply instantiated_busy_interval_prefix_equivalent_busy_interval_prefix => //.
+        - by apply workload_is_bounded => //.
+      Qed.
+
+    End Case1.
+
+    (** Next, we consider the case when the interval <<[t1, t1 + L)>>
+        is not a busy-interval prefix. *)
+    Section Case2.
+
+      (** Consider that <<[t1, job_arrival j]>> is a busy-interval prefix of [j]
+          and <<[t1, t1 + L)>> is _not_. *)
+      Hypothesis H_arrives : t1 <= job_arrival j.
+      Hypothesis H_busy_prefix_arr : busy_interval_prefix arr_seq sched j t1 (job_arrival j).+1.
+      Hypothesis H_no_busy_prefix_L : ~ busy_interval_prefix arr_seq sched j t1 (t1 + L).
+
+      (** From the properties of busy intervals, one can conclude that
+          [j]'s arrival time is less than [t1 + L]. *)
+      Local Lemma job_arrival_is_bounded :
+        job_arrival j < t1 + L.
+      Proof.
+        move_neq_up FF.
+        move: (H_busy_prefix_arr) (H_busy_prefix_arr) => PREFIX PREFIXA.
+        apply instantiated_busy_interval_prefix_equivalent_busy_interval_prefix in PREFIXA => //.
+        move: (PREFIXA) => GTC.
+        eapply workload_exceeds_interval with (Δ := L) in PREFIX => //.
+        { move_neq_down PREFIX.
+          rewrite (cumulative_interfering_workload_split _ _ _).
+          rewrite (leqRW (blackout_during_bound _ _ _ _ _ _ _ _ (job_arrival j).+1 _ _ _)); (try apply H_valid_SBF) => //.
+          rewrite addnC -!addnA.
+          have E: forall a b c, a <= c -> b <= c - a -> a + b <= c by move => ? ? ? ? ?; lia.
+          apply: E; first by lia.
+          rewrite subKn; last by apply: sbf_bounded_by_duration => //.
+          specialize (H_fixed_point (job_arrival j - t1)).
+          rewrite -(leqRW H_fixed_point); apply leq_add.
+          { rewrite (leqRW (service_inversion_widen _ _ _ t1 _ _ (job_arrival j).+1 _ _ )).
+            - apply: leq_trans.
+              + apply: service_inversion_is_bounded => //.
+                move => *; instantiate (1 := fun (A : duration) => blocking_bound ts tsk A) => //.
+                by apply: nonpreemptive_segments_bounded_by_blocking => //.
+              + by done.
+            - by done.
+            - lia.
+          }
+          { rewrite addnC cumulative_iw_hep_eq_workload_of_ohep workload_job_and_ahep_eq_workload_hep //.
+            apply workload_of_jobs_bounded => //.
+            move=> j'.
+            move: H_job_of_tsk => /eqP <-.
+            by apply hep_job_implies_hep_task. }
+        }
+      Qed.
+
+      (** Lemma [job_arrival_is_bounded] implies that the
+          busy-interval prefix starts at time [t1], continues until
+          [job_arrival j + 1], and then terminates before [t1 + L].
+          Or, in other words, there is point in time [t2] such that
+          (1) [j]'s arrival is bounded by [t2], (2) [t2] is bounded by
+          [t1 + L], and (3) <<[t1, t2)>> is the busy interval of job
+          [j]. *)
+      Local Lemma busy_prefix_is_bounded_case2:
+        exists t2, job_arrival j < t2 /\ t2 <= t1 + L /\ busy_interval arr_seq sched j t1 t2.
+      Proof.
+        have LE: job_arrival j < t1 + L
+          by apply job_arrival_is_bounded => //; try apply instantiated_busy_interval_prefix_equivalent_busy_interval_prefix.
+        move: (H_busy_prefix_arr) => PREFIX.
+        move: (H_no_busy_prefix_L) => NOPREF.
+        apply instantiated_busy_interval_prefix_equivalent_busy_interval_prefix in PREFIX => //.
+        have BUSY := terminating_busy_prefix_is_busy_interval _ _ _ _ _ _ _ PREFIX.
+        edestruct BUSY as [t2 BUS]; clear BUSY; try apply TSK; eauto 2 => //.
+        { move => T; apply: NOPREF.
+          by apply instantiated_busy_interval_prefix_equivalent_busy_interval_prefix in T => //.
+        }
+        exists t2; split; last split.
+        { move: BUS => [[A _] _]; lia. }
+        { move_neq_up FA.
+          apply: NOPREF; split; [lia | split; first by apply H_busy_prefix_arr].
+          split.
+          - move=> t NEQ.
+            apply abstract_busy_interval_classic_busy_interval_prefix in BUS => //.
+            by apply BUS; lia.
+          - lia.
+        }
+        { by apply instantiated_busy_interval_equivalent_busy_interval => //. }
+      Qed.
+
+    End Case2.
+
+  End StepByStepProof.
+
+  (** Combining the cases analyzed above, we conclude that busy
+      intervals of jobs released by task [tsk] are bounded by [L].  *)
+  Lemma busy_intervals_are_bounded_rs_elf :
+    busy_intervals_are_bounded_by arr_seq sched tsk L.
+  Proof.
+    move => j ARR TSK POS.
+    have PEND : pending sched j (job_arrival j) by apply job_pending_at_arrival => //.
+    have [t1 [GE PREFIX]]:
+      exists t1, t1 <= job_arrival j
+            /\ busy_interval_prefix arr_seq sched j t1 (job_arrival j).+1
+        by apply: busy_interval_prefix_exists.
+    exists t1.
+    enough(exists t2, job_arrival j < t2 /\ t2 <= t1 + L /\ busy_interval arr_seq sched j t1 t2) as BUSY.
+    { move: BUSY => [t2 [LT [LE BUSY]]]; eexists; split; last first.
+      { split; first by exact: LE.
+        by apply instantiated_busy_interval_equivalent_busy_interval. }
+      { by apply/andP; split. }
+    }
+    { have [LPREF|NOPREF] := busy_interval_prefix_case ltac:(eauto) j t1 (t1 + L).
+      { apply busy_prefix_is_bounded_case1 => //.
+        by apply instantiated_busy_interval_prefix_equivalent_busy_interval_prefix => //. }
+      { apply busy_prefix_is_bounded_case2=> //.
+        move=> NP; apply: NOPREF.
+        by apply instantiated_busy_interval_prefix_equivalent_busy_interval_prefix => //.
+      }
+    }
+  Qed.
+
+End BoundedBusyIntervals.

analysis/abstract/restricted_supply/bounded_bi/fp.v

+Require Export prosa.analysis.facts.blocking_bound.fp.
+Require Export prosa.analysis.abstract.restricted_supply.abstract_rta.
+Require Export prosa.analysis.abstract.restricted_supply.iw_instantiation.
+Require Export prosa.analysis.abstract.restricted_supply.bounded_bi.aux.
+Require Export prosa.analysis.definitions.sbf.busy.
+
+
+(** * Sufficient Condition for Bounded Busy Intervals for RS FP *)
+
+(** In this section, we show that the existence of [L] such that [B +
+    total_hep_rbf L <= SBF L], where [B] is the blocking bound and
+    [SBF] is a supply-bound function, is a sufficient condition for
+    the existence of bounded busy intervals under FP scheduling with a
+    restricted-supply processor model. *)
+Section BoundedBusyIntervals.
+
+  (** 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 any kind of fully supply-consuming unit-supply
+      uniprocessor model. *)
+  Context `{PState : ProcessorState Job}.
+  Hypothesis H_uniprocessor_proc_model : uniprocessor_model PState.
+  Hypothesis H_unit_supply_proc_model : unit_supply_proc_model PState.
+  Hypothesis H_consumed_supply_proc_model : fully_consuming_proc_model PState.
+
+  (** Consider an FP policy that indicates a higher-or-equal priority
+      relation, and assume that the relation is reflexive and
+      transitive. *)
+  Context {FP : FP_policy Task}.
+  Hypothesis H_priority_is_reflexive : reflexive_task_priorities FP.
+  Hypothesis H_priority_is_transitive : transitive_task_priorities FP.
+
+  (** Consider any valid arrival sequence. *)
+  Variable arr_seq : arrival_sequence Job.
+  Hypothesis H_valid_arrival_sequence : valid_arrival_sequence arr_seq.
+
+  (** Next, consider a schedule of this arrival sequence, ... *)
+  Variable sched : schedule PState.
+
+  (** ... allow for any work-bearing notion of job readiness, ... *)
+  Context `{!JobReady Job PState}.
+  Hypothesis H_job_ready : work_bearing_readiness arr_seq sched.
+
+  (** ... and assume that the schedule is valid. *)
+  Hypothesis H_sched_valid : valid_schedule sched arr_seq.
+
+  (** Assume that jobs have bounded non-preemptive segments. *)
+  Context `{JobPreemptable Job}.
+  Context `{TaskMaxNonpreemptiveSegment Task}.
+  Hypothesis H_valid_preemption_model : valid_preemption_model arr_seq sched.
+  Hypothesis H_valid_model_with_bounded_nonpreemptive_segments :
+    valid_model_with_bounded_nonpreemptive_segments arr_seq sched.
+
+  (** Furthermore, assume that the schedule respects the scheduling policy. *)
+  Hypothesis H_respects_policy : respects_FP_policy_at_preemption_point arr_seq sched FP.
+
+  (** Recall that [busy_intervals_are_bounded_by] is an abstract
+      notion. Hence, we need to introduce interference and interfering
+      workload. We will use the restricted-supply instantiations. *)
+
+  (** We say that job [j] incurs interference at time [t] iff it
+      cannot execute due to (1) the lack of supply at time [t], (2)
+      service inversion (i.e., a lower-priority job receiving service
+      at [t]), or a higher-or-equal-priority job receiving service. *)
+  #[local] Instance rs_jlfp_interference : Interference Job :=
+    rs_jlfp_interference arr_seq sched.
+
+  (** The interfering workload, in turn, is defined as the sum of the
+      blackout predicate, service inversion predicate, and the
+      interfering workload of jobs with higher or equal priority. *)
+  #[local] Instance rs_jlfp_interfering_workload : InterferingWorkload Job :=
+    rs_jlfp_interfering_workload arr_seq sched.
+
+  (** Assume that the schedule is work-conserving in the abstract sense. *)
+  Hypothesis H_work_conserving : definitions.work_conserving arr_seq sched.
+
+  (** Consider an arbitrary task set [ts], ... *)
+  Variable ts : list Task.
+
+  (** ... assume that all jobs come from the task set, ... *)
+  Hypothesis H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts.
+
+  (** ... and that the cost of a job does not exceed its task's WCET. *)
+  Hypothesis H_valid_job_cost : arrivals_have_valid_job_costs arr_seq.
+
+  (** 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.
+  Hypothesis H_is_arrival_curve : taskset_respects_max_arrivals arr_seq ts.
+
+  (** Let [tsk] be any task in [ts] that is to be analyzed. *)
+  Variable tsk : Task.
+  Hypothesis H_tsk_in_ts : tsk \in ts.
+
+  (** Consider a unit SBF valid in busy intervals (w.r.t. task
+      [tsk]). That is, (1) [SBF 0 = 0], (2) for any duration [Δ], the
+      supply produced during a busy-interval prefix of length [Δ] is
+      at least [SBF Δ], and (3) [SBF] makes steps of at most one. *)
+  Context {SBF : SupplyBoundFunction}.
+  Hypothesis H_valid_SBF : valid_busy_sbf arr_seq sched tsk SBF.
+  Hypothesis H_unit_SBF : unit_supply_bound_function SBF.
+
+  (** Let [L] be any positive fixed point of the busy-interval recurrence. *)
+  Variable L : duration.
+  Hypothesis H_L_positive : 0 < L.
+  Hypothesis H_fixed_point :
+    blocking_bound ts tsk + total_hep_request_bound_function_FP ts tsk L <= SBF L.
+
+  (** Next, we provide a step-by-step proof of busy-interval boundedness. *)
+  Section StepByStepProof.
+
+    (** Consider any job [j] of task [tsk] that has a positive job
+        cost and is in the arrival sequence. *)
+    Variable j : Job.
+    Hypothesis H_j_arrives : arrives_in arr_seq j.
+    Hypothesis H_job_of_tsk : job_of_task tsk j.
+    Hypothesis H_job_cost_positive : job_cost_positive j.
+
+    (** Consider two cases: (1) when the busy-interval prefix
+        continues until time instant [t1 + L] and (2) when the busy
+        interval prefix terminates earlier. In either case, we can
+        show that the busy-interval prefix is bounded. *)
+
+    (** We start with the first case, where the busy-interval prefix
+        continues until time instant [t1 + L]. *)
+    Section Case1.
+
+      (** Consider a time instant [t1] such that <<[t1, job_arrival
+          j]>> and <<[t1, t1 + L)>> are both busy-interval prefixes of
+          job [j].
+
+          Note that at this point we do not necessarily know that
+          [job_arrival j <= L]; hence, we assume the existence of both
+          prefixes. *)
+      Variable t1 : instant.
+      Hypothesis H_busy_prefix_arr : busy_interval_prefix arr_seq sched j t1 (job_arrival j).+1.
+      Hypothesis H_busy_prefix_L : busy_interval_prefix arr_seq sched j t1 (t1 + L).
+
+      (** The crucial point to note is that the sum of the job's cost
+          (represented as [workload_of_job]) and the interfering
+          workload in the interval <<[t1, t1 + L)>> is bounded by [L]
+          due to the fixed point [H_fixed_point]. *)
+      Local Lemma workload_is_bounded :
+        workload_of_job arr_seq j t1 (t1 + L) + cumulative_interfering_workload j t1 (t1 + L) <= L.
+      Proof.
+        rewrite (cumulative_interfering_workload_split _ _ _).
+        rewrite (leqRW (blackout_during_bound _ _ _ _ _ _ _ _ (t1 + L) _ _ _)); (try apply H_valid_SBF) => //.
+        rewrite // addnC -!addnA.
+        have E: forall a b c, a <= c -> b <= c - a -> a + b <= c by move => ? ? ? ? ?; lia.
+        apply: E; first by lia.
+        rewrite subKn; last by apply: sbf_bounded_by_duration => //.
+        rewrite -(leqRW H_fixed_point); apply leq_add.
+        - apply: leq_trans; first apply: service_inversion_is_bounded => //.
+          + instantiate (1 := fun _ => blocking_bound ts tsk) => //=.
+            by move=> jo t t' ARRo TSKo PREFo; apply: nonpreemptive_segments_bounded_by_blocking => //.
+          + by done.
+        - rewrite addnC cumulative_iw_hep_eq_workload_of_ohep workload_job_and_ahep_eq_workload_hep //.
+          by apply hep_workload_le_total_hep_rbf.
+      Qed.
+
+      (** It follows that [t1 + L] is a quiet time, which means that
+          the busy prefix ends (i.e., it is bounded). *)
+      Local Lemma busy_prefix_is_bounded_case1 :
+        exists t2,
+          job_arrival j < t2
+          /\ t2 <= t1 + L
+          /\ busy_interval arr_seq sched j t1 t2.
+      Proof.
+        have PEND : pending sched j (job_arrival j) by apply job_pending_at_arrival => //.
+        enough(exists t2, job_arrival j < t2 /\ t2 <= t1 + L /\ definitions.busy_interval sched j t1 t2) as BUSY.
+        { have [t2 [LE1 [LE2 BUSY2]]] := BUSY.
+          eexists; split; first by exact: LE1.
+          split; first by done.
+          by apply instantiated_busy_interval_equivalent_busy_interval.
+        }
+        eapply busy_interval.busy_interval_is_bounded; eauto 2 => //.
+        - by eapply instantiated_i_and_w_no_speculative_execution; eauto 2 => //.
+        - by apply instantiated_busy_interval_prefix_equivalent_busy_interval_prefix => //.
+        - by apply workload_is_bounded => //.
+      Qed.
+
+    End Case1.
+
+    (** Next, we consider the case when the interval <<[t1, t1 + L)>>
+        is not a busy-interval prefix. *)
+    Section Case2.
+
+      (** Consider a time instant [t1] such that <<[t1, job_arrival
+          j]>> is a busy-interval prefix of [j] and <<[t1, t1 + L)>>
+          is _not_. *)
+      Variable t1 : instant.
+      Hypothesis H_arrives : t1 <= job_arrival j.
+      Hypothesis H_busy_prefix_arr : busy_interval_prefix arr_seq sched j t1 (job_arrival j).+1.
+      Hypothesis H_no_busy_prefix_L : ~ busy_interval_prefix arr_seq sched j t1 (t1 + L).
+
+      (** From the properties of busy intervals, one can conclude that
+          [j]'s arrival time is less than [t1 + L]. *)
+      Local Lemma job_arrival_is_bounded :
+        job_arrival j < t1 + L.
+      Proof.
+        move_neq_up FF.
+        move: (H_busy_prefix_arr) (H_busy_prefix_arr) => PREFIX PREFIXA.
+        apply instantiated_busy_interval_prefix_equivalent_busy_interval_prefix in PREFIXA => //.
+        move: (PREFIXA) => GTC.
+        eapply workload_exceeds_interval with (Δ := L) in PREFIX => //.
+        { move_neq_down PREFIX.
+          rewrite (cumulative_interfering_workload_split _ _ _).
+          rewrite (leqRW (blackout_during_bound _ _ _ _ _ _ _ _ (job_arrival j).+1 _ _ _)); (try apply H_valid_SBF) => //.
+          rewrite addnC -!addnA.
+          have E: forall a b c, a <= c -> b <= c - a -> a + b <= c by move => ? ? ? ? ?; lia.
+          apply: E; first by lia.
+          rewrite subKn; last by apply: sbf_bounded_by_duration => //.
+          rewrite -(leqRW H_fixed_point); apply leq_add.
+          { rewrite (leqRW (service_inversion_widen _ _ _ t1 _ _ (job_arrival j).+1 _ _ )).
+            - apply: leq_trans.
+              + apply: service_inversion_is_bounded => //.
+                move => *; instantiate (1 := fun _ => blocking_bound ts tsk) => //.
+                by apply: nonpreemptive_segments_bounded_by_blocking => //.
+              + by done.
+            - by done.
+            - lia.
+          }
+          { rewrite addnC cumulative_iw_hep_eq_workload_of_ohep workload_job_and_ahep_eq_workload_hep //.
+            by apply hep_workload_le_total_hep_rbf. }
+        }
+      Qed.
+
+      (** Lemma [job_arrival_is_bounded] implies that the
+          busy-interval prefix starts at time [t1], continues until
+          [job_arrival j + 1], and then terminates before [t1 + L].
+          Or, in other words, there is point in time [t2] such that
+          (1) [j]'s arrival is bounded by [t2], (2) [t2] is bounded by
+          [t1 + L], and (3) <<[t1, t2)>> is busy interval of job
+          [j]. *)
+      Local Lemma busy_prefix_is_bounded_case2:
+        exists t2, job_arrival j < t2 /\ t2 <= t1 + L /\ busy_interval arr_seq sched j t1 t2.
+      Proof.
+        have LE: job_arrival j < t1 + L
+          by apply job_arrival_is_bounded => //; try apply instantiated_busy_interval_prefix_equivalent_busy_interval_prefix.
+        move: (H_busy_prefix_arr) => PREFIX.
+        move: (H_no_busy_prefix_L) => NOPREF.
+        apply instantiated_busy_interval_prefix_equivalent_busy_interval_prefix in PREFIX => //.
+        have BUSY := terminating_busy_prefix_is_busy_interval _ _ _ _ _ _ _ PREFIX.
+        edestruct BUSY as [t2 BUS]; clear BUSY; try apply TSK; eauto 2 => //.
+        { move => T; apply: NOPREF.
+          by apply instantiated_busy_interval_prefix_equivalent_busy_interval_prefix in T => //.
+        }
+        exists t2; split; last split.
+        { move: BUS => [[A _] _]; lia. }
+        { move_neq_up FA.
+          apply: NOPREF; split; [lia | split; first by apply H_busy_prefix_arr].
+          split.
+          - move=> t NEQ.
+            apply abstract_busy_interval_classic_busy_interval_prefix in BUS => //.
+            by apply BUS; lia.
+          - lia.
+        }
+        { by apply instantiated_busy_interval_equivalent_busy_interval => //. }
+      Qed.
+
+    End Case2.
+
+  End StepByStepProof.
+
+  (** Combining the cases analyzed above, we conclude that busy
+      intervals of jobs released by task [tsk] are bounded by [L].  *)
+  Lemma busy_intervals_are_bounded_rs_fp :
+    busy_intervals_are_bounded_by arr_seq sched tsk L.
+  Proof.
+    move => j ARR TSK POS.
+    have PEND : pending sched j (job_arrival j) by apply job_pending_at_arrival => //.
+    have [t1 [GE PREFIX]]:
+      exists t1, t1 <= job_arrival j
+            /\ busy_interval_prefix arr_seq sched j t1 (job_arrival j).+1
+        by apply: busy_interval_prefix_exists.
+    exists t1.
+    enough(exists t2, job_arrival j < t2 /\ t2 <= t1 + L /\ busy_interval arr_seq sched j t1 t2) as BUSY.
+    { move: BUSY => [t2 [LT [LE BUSY]]]; eexists; split; last first.
+      { split; first by exact: LE.
+        by apply instantiated_busy_interval_equivalent_busy_interval. }
+      { by apply/andP; split. }
+    }
+    { have [LPREF|NOPREF] := busy_interval_prefix_case ltac:(eauto) j t1 (t1 + L).
+      { apply busy_prefix_is_bounded_case1 => //.
+        by apply instantiated_busy_interval_prefix_equivalent_busy_interval_prefix => //. }
+      { apply busy_prefix_is_bounded_case2=> //.
+        move=> NP; apply: NOPREF.
+        by apply instantiated_busy_interval_prefix_equivalent_busy_interval_prefix => //.
+      }
+    }
+  Qed.
+
+End BoundedBusyIntervals.
+

analysis/abstract/restricted_supply/bounded_bi/jlfp.v

+Require Export prosa.analysis.abstract.restricted_supply.abstract_rta.
+Require Export prosa.analysis.abstract.restricted_supply.iw_instantiation.
+Require Export prosa.analysis.abstract.restricted_supply.bounded_bi.aux.
+Require Export prosa.analysis.facts.busy_interval.carry_in.
+Require Export prosa.analysis.definitions.sbf.busy.
+
+
+(** * Sufficient Condition for Bounded Busy Intervals for RS JLFP *)
+
+(** In this section, we show that the existence of [L] such that [B +
+    total_rbf L <= SBF L], where where [B] is the blocking bound and
+    [SBF] is a supply-bound function, is a sufficient condition for
+    the existence of bounded busy intervals under JLFP scheduling with
+    a restricted-supply processor model. Note that this is not the
+    tightest bound, but it can be useful in case the blocking bound is
+    small or zero.  *)
+Section BoundedBusyIntervals.
+
+  (** 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 any kind of fully supply-consuming unit-supply
+      uniprocessor model. *)
+  Context `{PState : ProcessorState Job}.
+  Hypothesis H_uniprocessor_proc_model : uniprocessor_model PState.
+  Hypothesis H_unit_supply_proc_model : unit_supply_proc_model PState.
+  Hypothesis H_consumed_supply_proc_model : fully_consuming_proc_model PState.
+
+  (** Consider a JLFP policy that indicates a higher-or-equal priority
+      relation, and assume that the relation is reflexive and
+      transitive. *)
+  Context {JLFP : JLFP_policy Job}.
+  Hypothesis H_priority_is_reflexive : reflexive_job_priorities JLFP.
+  Hypothesis H_priority_is_transitive : transitive_job_priorities JLFP.
+
+  (** Consider any valid arrival sequence. *)
+  Variable arr_seq : arrival_sequence Job.
+  Hypothesis H_valid_arrival_sequence : valid_arrival_sequence arr_seq.
+
+  (** Next, consider a schedule of this arrival sequence, ... *)
+  Variable sched : schedule PState.
+
+  (** ... allow for any work-bearing notion of job readiness, ... *)
+  Context `{!JobReady Job PState}.
+  Hypothesis H_job_ready : work_bearing_readiness arr_seq sched.
+
+  (** ... and assume that the schedule is valid. *)
+  Hypothesis H_sched_valid : valid_schedule sched arr_seq.
+
+  (** Assume that jobs have bounded non-preemptive segments. *)
+  Context `{JobPreemptable Job}.
+  Context `{TaskMaxNonpreemptiveSegment Task}.
+  Hypothesis H_valid_preemption_model : valid_preemption_model arr_seq sched.
+  Hypothesis H_valid_model_with_bounded_nonpreemptive_segments :
+    valid_model_with_bounded_nonpreemptive_segments arr_seq sched.
+
+  (** Recall that [busy_intervals_are_bounded_by] is an abstract
+      notion. Hence, we need to introduce interference and interfering
+      workload. We will use the restricted-supply instantiations. *)
+
+  (** We say that job [j] incurs interference at time [t] iff it
+      cannot execute due to (1) the lack of supply at time [t], (2)
+      service inversion (i.e., a lower-priority job receiving service
+      at [t]), or a higher-or-equal-priority job receiving service. *)
+  #[local] Instance rs_jlfp_interference : Interference Job :=
+    rs_jlfp_interference arr_seq sched.
+
+  (** The interfering workload, in turn, is defined as the sum of the
+      blackout predicate, service inversion predicate, and the
+      interfering workload of jobs with higher or equal priority. *)
+  #[local] Instance rs_jlfp_interfering_workload : InterferingWorkload Job :=
+    rs_jlfp_interfering_workload arr_seq sched.
+
+  (** In the following, we assume that the scheduler is work-conserving in the
+      abstract sense. *)
+  Hypothesis H_work_conserving : abstract.definitions.work_conserving arr_seq sched.
+
+  (** Consider an arbitrary task set [ts], ... *)
+  Variable ts : list Task.
+
+  (** ... assume that all jobs come from the task set, ... *)
+  Hypothesis H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts.
+
+  (** ... and that the cost of a job does not exceed its task's WCET. *)
+  Hypothesis H_valid_job_cost : arrivals_have_valid_job_costs arr_seq.
+
+  (** Let [max_arrivals] be a family of valid arrival curves. *)
+  Context `{MaxArrivals Task}.
+  Hypothesis H_is_arrival_curve : taskset_respects_max_arrivals arr_seq ts.
+
+  (** Let [tsk] be any task in [ts] that is to be analyzed. *)
+  Variable tsk : Task.
+  Hypothesis H_tsk_in_ts : tsk \in ts.
+
+  (** Consider a unit SBF valid in busy intervals (w.r.t. task
+      [tsk]). That is, (1) [SBF 0 = 0], (2) for any duration [Δ], the
+      supply produced during a busy-interval prefix of length [Δ] is
+      at least [SBF Δ], and (3) [SBF] makes steps of at most one. *)
+  Context {SBF : SupplyBoundFunction}.
+  Hypothesis H_valid_SBF : valid_busy_sbf arr_seq sched tsk SBF.
+  Hypothesis H_unit_SBF : unit_supply_bound_function SBF.
+
+  (** Let [blocking_bound] be a function that bounds the priority
+      inversion caused by lower-priority jobs, where the argument
+      [blocking_bound] takes is the relative offset (w.r.t. the
+      beginning of the corresponding busy interval) of a job to be
+      analyzed. *)
+  Variable blocking_bound : (* A *) duration -> duration.
+
+  (** Assume that the service inversion is bounded by the blocking
+      bound, ... *)
+  Hypothesis H_service_inversion_bounded :
+    service_inversion_is_bounded_by arr_seq sched tsk blocking_bound.
+
+  (** ... and that [blocking_bound] reaches its maximum at [0]. *)
+  Hypothesis H_blocking_bound_max :
+    forall A, blocking_bound 0 >= blocking_bound A.
+
+  (** Let [L] be any positive fixed point of busy-interval recurrence
+      [blocking_bound 0 + total_rbf ts L <= SBF L]. *)
+  Variable L : duration.
+  Hypothesis H_L_positive : 0 < L.
+  Hypothesis H_fixed_point :
+    blocking_bound 0 + total_request_bound_function ts L <= SBF L.
+
+  (** Next, we provide a step-by-step proof of busy-interval boundedness. *)
+  Section StepByStepProof.
+
+    (** Consider any job [j] of task [tsk] that has a positive job
+        cost and is in the arrival sequence. *)
+    Variable j : Job.
+    Hypothesis H_j_arrives : arrives_in arr_seq j.
+    Hypothesis H_job_of_tsk : job_of_task tsk j.
+    Hypothesis H_job_cost_positive : job_cost_positive j.
+
+    (** We consider two cases: (1) when the busy-interval prefix
+        continues until time instant [t1 + L] and (2) when the busy
+        interval prefix terminates earlier. In either case, we can
+        show that the busy-interval prefix is bounded. *)
+
+    (** We start with the first case, where the busy-interval prefix
+        continues until time instant [t1 + L]. *)
+    Section Case1.
+
+      (** Consider a time instant [t1] such that <<[t1, job_arrival
+          j]>> and <<[t1, t1 + L)>> are both busy-interval prefixes of
+          job [j].
+
+          Note that at this point we do not necessarily know that
+          [job_arrival j <= L]; hence, in this section (only), we
+          assume the existence of both prefixes. *)
+      Variable t1 : instant.
+      Hypothesis H_busy_prefix_arr : busy_interval_prefix arr_seq sched j t1 (job_arrival j).+1.
+      Hypothesis H_busy_prefix_L : busy_interval_prefix arr_seq sched j t1 (t1 + L).
+
+      (** The crucial point to note is that the sum of the job's cost
+          (represented as [workload_of_job]) and the interfering
+          workload in the interval <<[t1, t1 + L)>> is bounded by [L]
+          due to the fixed point [H_fixed_point]. *)
+      Local Lemma workload_is_bounded :
+        workload_of_job arr_seq j t1 (t1 + L) + cumulative_interfering_workload j t1 (t1 + L) <= L.
+      Proof.
+        rewrite (cumulative_interfering_workload_split _ _ _).
+        rewrite (leqRW (blackout_during_bound _ _ _ _ _ _ _ _ (t1 + L) _ _ _)); (try apply H_valid_SBF) => //.
+        rewrite // addnC -!addnA.
+        have E: forall a b c, a <= c -> b <= c - a -> a + b <= c by move => ? ? ? ? ?; lia.
+        apply: E; first by lia.
+        rewrite subKn; last by apply: sbf_bounded_by_duration => //.
+        rewrite -(leqRW H_fixed_point); apply leq_add.
+        - by rewrite (leqRW (H_service_inversion_bounded _ _ _ _ _ _ _)) //=.
+        - rewrite addnC cumulative_iw_hep_eq_workload_of_ohep workload_job_and_ahep_eq_workload_hep //.
+          by apply hep_workload_le_total_rbf.
+      Qed.
+
+      (** It follows that [t1 + L] is a quiet time, which means that
+          the busy prefix ends (i.e., it is bounded). *)
+      Local Lemma busy_prefix_is_bounded_case1 :
+        exists t2,
+          job_arrival j < t2
+          /\ t2 <= t1 + L
+          /\ busy_interval arr_seq sched j t1 t2.
+      Proof.
+        have PEND : pending sched j (job_arrival j) by apply job_pending_at_arrival => //.
+        enough(exists t2, job_arrival j < t2 /\ t2 <= t1 + L /\ definitions.busy_interval sched j t1 t2) as BUSY.
+        { have [t2 [LE1 [LE2 BUSY2]]] := BUSY.
+          eexists; split; first by exact: LE1.
+          split; first by done.
+          by apply instantiated_busy_interval_equivalent_busy_interval.
+        }
+        eapply busy_interval.busy_interval_is_bounded; eauto 2 => //.
+        - by eapply instantiated_i_and_w_no_speculative_execution; eauto 2 => //.
+        - by apply instantiated_busy_interval_prefix_equivalent_busy_interval_prefix => //.
+        - by apply workload_is_bounded => //.
+      Qed.
+
+    End Case1.
+
+    (** Next, we consider the case when the interval <<[t1, t1 + L)>>
+        is not a busy-interval prefix. *)
+    Section Case2.
+
+      (** Consider a time instant [t1] such that <<[t1, job_arrival
+          j]>> is a busy-interval prefix of [j] and <<[t1, t1 + L)>>
+          is _not_. *)
+      Variable t1 : instant.
+      Hypothesis H_arrives : t1 <= job_arrival j.
+      Hypothesis H_busy_prefix_arr : busy_interval_prefix arr_seq sched j t1 (job_arrival j).+1.
+      Hypothesis H_no_busy_prefix_L : ~ busy_interval_prefix arr_seq sched j t1 (t1 + L).
+
+      (** From the properties of busy intervals, one can conclude that
+          [j]'s arrival time is less than [t1 + L]. *)
+      Local Lemma job_arrival_is_bounded :
+        job_arrival j < t1 + L.
+      Proof.
+        move_neq_up FF.
+        move: (H_busy_prefix_arr) (H_busy_prefix_arr) => PREFIX PREFIXA.
+        apply instantiated_busy_interval_prefix_equivalent_busy_interval_prefix in PREFIXA => //.
+        move: (PREFIXA) => GTC.
+        eapply workload_exceeds_interval with (Δ := L) in PREFIX => //.
+        { move_neq_down PREFIX.
+          rewrite (cumulative_interfering_workload_split _ _ _).
+          rewrite (leqRW (blackout_during_bound _ _ _ _ _ _ _ _ (job_arrival j).+1 _ _ _)); (try apply H_valid_SBF) => //.
+          rewrite addnC -!addnA.
+          have E: forall a b c, a <= c -> b <= c - a -> a + b <= c by move => ? ? ? ? ?; lia.
+          apply: E; first by lia.
+          rewrite subKn; last by apply: sbf_bounded_by_duration => //.
+          rewrite -(leqRW H_fixed_point); apply leq_add.
+          { rewrite (leqRW (service_inversion_widen _ _ _ t1 _ _ (job_arrival j).+1 _ _ )).
+            - by rewrite (leqRW (H_service_inversion_bounded _ _ _ _ _ _ _)) //=.
+            - by done.
+            - by lia.
+          }
+          { rewrite addnC cumulative_iw_hep_eq_workload_of_ohep workload_job_and_ahep_eq_workload_hep //.
+            by apply hep_workload_le_total_rbf.
+          }
+        }
+      Qed.
+
+      (** Lemma [job_arrival_is_bounded] implies that the
+          busy-interval prefix starts at time [t1], continues until
+          [job_arrival j + 1], and then terminates before [t1 + L].
+          Or, in other words, there is point in time [t2] such that
+          (1) [j]'s arrival is bounded by [t2], (2) [t2] is bounded by
+          [t1 + L], and (3) <<[t1, t2)>> is busy interval of job
+          [j]. *)
+      Local Lemma busy_prefix_is_bounded_case2:
+        exists t2, job_arrival j < t2 /\ t2 <= t1 + L /\ busy_interval arr_seq sched j t1 t2.
+      Proof.
+        have LE: job_arrival j < t1 + L
+          by apply job_arrival_is_bounded => //; try apply instantiated_busy_interval_prefix_equivalent_busy_interval_prefix.
+        move: (H_busy_prefix_arr) => PREFIX.
+        move: (H_no_busy_prefix_L) => NOPREF.
+        apply instantiated_busy_interval_prefix_equivalent_busy_interval_prefix in PREFIX => //.
+        have BUSY := terminating_busy_prefix_is_busy_interval _ _ _ _ _ _ _ PREFIX.
+        edestruct BUSY as [t2 BUS]; clear BUSY; try apply TSK; eauto 2 => //.
+        { move => T; apply: NOPREF.
+          by apply instantiated_busy_interval_prefix_equivalent_busy_interval_prefix in T => //.
+        }
+        exists t2; split; last split.
+        { by move: BUS => [[A _] _]; lia. }
+        { move_neq_up FA.
+          apply: NOPREF; split; [lia | split; first by apply H_busy_prefix_arr].
+          split.
+          - move=> t NEQ.
+            apply abstract_busy_interval_classic_busy_interval_prefix in BUS => //.
+            by apply BUS; lia.
+          - by lia.
+        }
+        { by apply instantiated_busy_interval_equivalent_busy_interval => //. }
+      Qed.
+
+    End Case2.
+
+  End StepByStepProof.
+
+  (** Combining the cases analyzed above, we conclude that busy
+      intervals of jobs released by task [tsk] are bounded by [L].  *)
+  Lemma busy_intervals_are_bounded_rs_jlfp :
+    busy_intervals_are_bounded_by arr_seq sched tsk L.
+  Proof.
+    move => j ARR TSK POS.
+    have PEND : pending sched j (job_arrival j) by apply job_pending_at_arrival => //.
+    edestruct ( busy_interval_prefix_exists) as [t1 [GE PREFIX]]; eauto 2.
+    exists t1.
+    enough(exists t2, job_arrival j < t2 /\ t2 <= t1 + L /\ busy_interval arr_seq sched j t1 t2) as BUSY.
+    { move: BUSY => [t2 [LT [LE BUSY]]]; eexists; split; last first.
+      { split; first by exact: LE.
+        by apply instantiated_busy_interval_equivalent_busy_interval. }
+      { by apply/andP; split. }
+    }
+    { have [LPREF|NOPREF] := busy_interval_prefix_case ltac:(eauto) j t1 (t1 + L).
+      { apply busy_prefix_is_bounded_case1 => //.
+        by apply instantiated_busy_interval_prefix_equivalent_busy_interval_prefix => //. }
+      { apply busy_prefix_is_bounded_case2=> //.
+        move=> NP; apply: NOPREF.
+        by apply instantiated_busy_interval_prefix_equivalent_busy_interval_prefix => //.
+      }
+    }
+  Qed.
+
+End BoundedBusyIntervals.

analysis/abstract/restricted_supply/busy_prefix.v

+Require Export prosa.model.priority.classes.
+Require Export prosa.analysis.facts.behavior.completion.
+Require Export prosa.analysis.definitions.service.
+Require Export prosa.analysis.definitions.service_inversion.pred.
+Require Export prosa.analysis.abstract.definitions.
+
+(** * Service Inversion Bounded *)
+(** In this section, we define the notion of bounded cumulative
+    service inversion in an abstract busy interval prefix. *)
+Section ServiceInversion.
+
+  (** 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}.
+
+  (** Next, consider _any_ kind of processor state model, ... *)
+  Context {PState : ProcessorState Job}.
+
+  (** ... any arrival sequence, ... *)
+  Variable arr_seq : arrival_sequence Job.
+
+  (** ... and any schedule of this arrival sequence. *)
+  Variable sched : schedule PState.
+
+  (** Assume we are provided with abstract functions for interference
+      and interfering workload. *)
+  Context `{Interference Job}.
+  Context `{InterferingWorkload Job}.
+
+  (** Assume a given JLFP policy. *)
+  Context `{JLFP_policy Job}.
+
+  (** If the priority inversion experienced by job [j] depends on its
+      relative arrival time w.r.t. the beginning of its busy interval
+      at a time [t1], we say that the service inversion of job [j] is
+      bounded by a function [B : duration -> duration] if the
+      cumulative service inversion within any (abstract) busy interval
+      prefix is bounded by [B (job_arrival j - t1)]. *)
+  Definition service_inversion_of_job_is_bounded_by (j : Job) (B : duration -> duration) :=
+    pred_service_inversion_of_job_is_bounded_by
+      arr_seq sched (busy_interval_prefix sched) j B.
+
+  (** We say that task [tsk] has bounded service inversion if all its
+      jobs have cumulative service inversion bounded by function [B :
+      duration -> duration], where [B] may depend on jobs' relative
+      arrival times w.r.t. the beginning of an abstract busy interval
+      prefix. *)
+  Definition service_inversion_is_bounded_by (tsk : Task) (B : duration -> duration) :=
+    pred_service_inversion_is_bounded_by
+      arr_seq sched (busy_interval_prefix sched) tsk B.
+
+End ServiceInversion.

analysis/abstract/restricted_supply/busy_sbf.v

+Require Export prosa.util.all.
+Require Export prosa.analysis.definitions.sbf.pred.
+Require Export prosa.analysis.abstract.definitions.
+
+(** * SBF within Abstract Busy Interval *)
+
+(** In the following, we define a weak notion of a supply bound
+    function, which is a valid SBF only within an abstract busy
+    interval of a task's job. *)
+Section BusySupplyBoundFunctions.
+
+  (** Consider any type of tasks, ... *)
+  Context {Task : TaskType}.
+
+  (** ... and any type of jobs. *)
+  Context {Job : JobType}.
+  Context `{JobArrival Job}.
+  Context `{JobCost Job}.
+  Context `{JobTask Job Task}.
+
+  (** ... any kind of processor state model, ... *)
+  Context `{PState : ProcessorState Job}.
+
+  (** ... any arrival sequence, ... *)
+  Variable arr_seq : arrival_sequence Job.
+
+  (** ... and any schedule. *)
+  Variable sched : schedule PState.
+
+  (** Consider a task [tsk]. *)
+  Variable tsk : Task.
+
+  (** Assume we are provided with abstract functions for Interference
+      and Interfering Workload. *)
+  Context `{Interference Job}.
+  Context `{InterferingWorkload Job}.
+
+  (** We define a predicate that determines whether an interval <<[t1,
+      t2)>> is a busy-interval prefix of a job [j] of task [tsk]. *)
+  Let bi_prefix_of_tsk j t1 t2 :=
+    job_of_task tsk j /\ busy_interval_prefix sched j t1 t2.
+
+  (** We say that the SBF is respected in a busy interval w.r.t. task
+      [tsk] if, for any busy interval <<[t1, t2)>> of a job [j ∈ tsk]
+      and a subinterval <<[t1, t) ⊆ [t1, t2)>>, at least [SBF (t -
+      t1)] cumulative supply is provided. *)
+  Definition sbf_respected_in_busy_interval (SBF : duration -> work) :=
+    pred_sbf_respected arr_seq sched bi_prefix_of_tsk SBF.
+
+  (** Next, we define an SBF that is valid within an (abstract) busy interval. *)
+  Definition valid_busy_sbf (SBF : duration -> work) :=
+    valid_pred_sbf arr_seq sched bi_prefix_of_tsk SBF.
+
+End BusySupplyBoundFunctions.

analysis/abstract/restricted_supply/iw_instantiation.v

+Require Export prosa.analysis.facts.interference.
+Require Export prosa.analysis.abstract.IBF.supply_task.
+Require Export prosa.analysis.facts.busy_interval.service_inversion.
+
+(** * JLFP Instantiation of Interference and Interfering Workload for Restricted-Supply Uniprocessor *)
+(** In this module we instantiate functions Interference and
+    Interfering Workload for the restricted-supply uni-processor
+    schedulers with an arbitrary JLFP-policy that satisfies the
+    sequential-tasks hypothesis. We also prove equivalence of
+    Interference and Interfering Workload to the more conventional
+    notions of service or workload. *)
+Section JLFPInstantiation.
+
+  (** 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 any kind of fully supply-consuming unit-supply
+      uniprocessor model. *)
+  Context `{PState : ProcessorState Job}.
+  Hypothesis H_uniprocessor_proc_model : uniprocessor_model PState.
+  Hypothesis H_unit_supply_proc_model : unit_supply_proc_model PState.
+  Hypothesis H_consumed_supply_proc_model : fully_consuming_proc_model PState.
+
+  (** Consider any valid arrival sequence with consistent arrivals... *)
+  Variable arr_seq : arrival_sequence Job.
+  Hypothesis H_valid_arrival_sequence : valid_arrival_sequence arr_seq.
+
+  (** ... and any valid uni-processor schedule of this arrival sequence... *)
+  Variable sched : schedule PState.
+  Hypothesis H_jobs_come_from_arrival_sequence :
+    jobs_come_from_arrival_sequence sched arr_seq.
+
+  (** ... where jobs do not execute before their arrival or after completion. *)
+  Hypothesis H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched.
+  Hypothesis H_completed_jobs_dont_execute : completed_jobs_dont_execute sched.
+
+  (** Consider a JLFP-policy that indicates a higher-or-equal priority
+      relation, and assume that this relation is reflexive and
+      transitive. *)
+  Context {JLFP : JLFP_policy Job}.
+  Hypothesis H_priority_is_reflexive : reflexive_job_priorities JLFP.
+
+  (** Let [tsk] be any task. *)
+  Variable tsk : Task.
+
+  (** * Interference and Interfering Workload *)
+  (** In the following, we introduce definitions of interference and
+      interfering workload. *)
+
+  (** ** Instantiation of Interference *)
+
+  (** We say that job [j] incurs interference at time [t] iff it
+      cannot execute due to (1) the lack of supply at time [t], (2)
+      due to service inversion (i.e., a lower-priority job receiving
+      service at [t]), or higher-or-equal-priority job receiving
+      service. *)
+  #[local] Instance rs_jlfp_interference : Interference Job :=
+    {
+      interference (j : Job) (t : instant) :=
+        is_blackout sched t
+        || service_inversion arr_seq sched j t
+        || another_hep_job_interference arr_seq sched j t
+    }.
+
+  (** ** Instantiation of Interfering Workload *)
+
+  (** The interfering workload, in turn, is defined as the sum of the
+      blackout predicate, service inversion predicate, and interfering
+      workload of jobs with higher or equal priority. *)
+  #[local] Instance rs_jlfp_interfering_workload : InterferingWorkload Job :=
+    {
+      interfering_workload (j : Job) (t : instant) :=
+        is_blackout sched t
+        + service_inversion arr_seq sched j t
+        + other_hep_jobs_interfering_workload arr_seq j t
+    }.
+
+  (** ** Equivalences *)
+
+  (** In this section we prove useful equivalences between the
+      definitions obtained by instantiation of definitions from the
+      Abstract RTA module (interference and interfering workload) and
+      definitions corresponding to the conventional concepts.
+
+      As it was mentioned previously, instantiated functions of
+      interference and interfering workload usually do not have any
+      useful lemmas about them. However, it is possible to prove their
+      equivalence to the more conventional notions like service or
+      workload. Next we prove the equivalence between the
+      instantiations and conventional notions. *)
+  Section Equivalences.
+
+    (** We prove that we can split cumulative interference into three
+        parts: (1) blackout time, (2) cumulative service inversion,
+        and (3) cumulative interference from jobs with higher or equal
+        priority. *)
+    Lemma cumulative_interference_split :
+      forall j t1 t2,
+        cumulative_interference j t1 t2
+        = blackout_during sched t1 t2
+          + cumulative_service_inversion arr_seq sched j t1 t2
+          + cumulative_another_hep_job_interference arr_seq sched j t1 t2.
+    Proof.
+      rewrite /cumulative_interference /cumul_cond_interference /rs_jlfp_interference /cond_interference /interference.
+      move=> j t1 t2; rewrite -big_split //= -big_split //=.
+      apply/eqP; rewrite eqn_leq; apply/andP; split; rewrite leq_sum//; move=> t _.
+      { by case is_blackout, service_inversion, another_hep_job_interference. }
+      { have [BL|SUP] := blackout_or_supply sched t.
+        { rewrite BL //= -addnA addnC addn1 ltnS leqn0 addn_eq0.
+          by apply/andP; split;
+            [rewrite eqb0 blackout_implies_no_service_inversion
+            | rewrite eqb0 no_hep_job_interference_without_supply]. }
+        { rewrite /is_blackout SUP //= add0n.
+          have [IDLE|[s SCHEDs]] := scheduled_at_cases arr_seq ltac:(eauto) sched ltac:(eauto) ltac:(eauto) t.
+          { by rewrite -[service_inversion _ _ _ _]negbK idle_implies_no_service_inversion //=. }
+          { rewrite (service_inversion_supply_sched _ _ _ _ _ _ _ _ _ _ s) //
+                    (interference_ahep_def _ _ _ _ _ _ _ _ _ _ s) //
+                    /another_hep_job.
+            have [EQ|NEQ] := eqVneq s j.
+            { by rewrite andbF orbF addn0. }
+            { by unfold hep_job_at, JLFP_to_JLDP, hep_job; rewrite andbT; case (JLFP s j) => //. }
+          }
+        }
+      }
+    Qed.
+
+    (** Similarly, we prove that we can split cumulative interfering
+        workload into three parts: (1) blackout time, (2) cumulative
+        service inversion, and (3) cumulative interfering workload
+        from jobs with higher or equal priority. *)
+    Lemma cumulative_interfering_workload_split :
+      forall j t1 t2,
+        cumulative_interfering_workload j t1 t2 =
+          blackout_during sched t1 t2
+          + cumulative_service_inversion arr_seq sched j t1 t2
+          + cumulative_other_hep_jobs_interfering_workload arr_seq j t1 t2.
+    Proof.
+      by move=> j t1 t2; rewrite -big_split //= -big_split //=.
+    Qed.
+
+    (** Let <<[t1, t2)>> be a time interval and let [j] be any job of
+        task [tsk] that is not completed by time [t2]. Then cumulative
+        interference received due jobs of other tasks executing can be
+        bounded by the sum of the cumulative service inversion of job
+        [j] and the cumulative interference incurred by task [tsk] due
+        to other tasks. *)
+    Lemma cumulative_task_interference_split :
+      forall j t1 t2,
+        arrives_in arr_seq j ->
+        job_of_task tsk j ->
+        ~~ completed_by sched j t2 ->
+        cumul_cond_interference (nonself_intra arr_seq sched) j t1 t2
+        <= cumulative_service_inversion arr_seq sched j t1 t2
+          + cumulative_another_task_hep_job_interference arr_seq sched j t1 t2.
+    Proof.
+      move=> j t1 R ARR TSK NCOMPL.
+      rewrite /cumul_task_interference /cumul_cond_interference.
+      rewrite -big_split //= big_seq_cond [leqRHS]big_seq_cond.
+      apply leq_sum; move => t /andP [IN _].
+      rewrite /cond_interference /nonself /interference /rs_jlfp_interference /nonself_intra.
+      have [SUP|NOSUP] := boolP (has_supply sched t); last first.
+      { by move: (NOSUP); rewrite /is_blackout => -> //=; rewrite andbT andbF //. }
+      { move: (SUP); rewrite /is_blackout => ->; rewrite andbT //=.
+        have [IDLE|[s SCHEDs]] := scheduled_at_cases arr_seq ltac:(eauto) sched ltac:(eauto) ltac:(eauto) t.
+        { rewrite /nonself.
+          by rewrite -[service_inversion _ _ _ _]negbK
+                     idle_implies_no_service_inversion //;
+             rewrite_neg no_hep_job_interference_when_idle;
+             rewrite_neg no_hep_task_interference_when_idle; rewrite andbF. }
+        { rewrite /nonself; move: (TSK) => /eqP ->.
+          erewrite task_served_at_eq_job_of_task => //; erewrite service_inversion_supply_sched => //.
+          erewrite interference_ahep_def => //.
+          erewrite interference_athep_def => //.
+          rewrite /another_hep_job /another_task_hep_job.
+          have [EQj|NEQj] := eqVneq s j.
+          { by subst; rewrite /job_of_task; move: TSK => /eqP => ->; rewrite H_priority_is_reflexive eq_refl. }
+          have [/eqP EQt|NEQt] := eqVneq (job_task s) (job_task j).
+          { rewrite /job_of_task; move: TSK => /eqP <-; rewrite EQt.
+            by apply/eqP; rewrite andbF andFb addn0 //=. }
+          { unfold hep_job_at, JLFP_to_JLDP, hep_job.
+            by rewrite /job_of_task; move: TSK => /eqP <-; rewrite NEQt //= andbT; case: JLFP. }
+        }
+      }
+    Qed.
+
+    (** We also show that the cumulative intra-supply interference can
+        be split into the sum of the cumulative service inversion and
+        cumulative interference incurred by the job due to other
+        higher-or-equal priority jobs. *)
+    Lemma cumulative_intra_interference_split :
+      forall j t1 t2,
+        cumul_cond_interference (fun (_j : Job) (t : instant) => has_supply sched t) j t1 t2
+        <= cumulative_service_inversion arr_seq sched j t1 t2
+          + cumulative_another_hep_job_interference arr_seq sched j t1 t2.
+    Proof.
+      move=> j t1 t2.
+      rewrite /cumul_cond_interference -big_split //= big_seq_cond [leqRHS]big_seq_cond.
+      apply leq_sum; move => t /andP [IN _].
+      rewrite /cond_interference /nonself /interference /rs_jlfp_interference.
+      have [SUP|NOSUP] := boolP (has_supply sched t); last first.
+      { by move: (NOSUP); rewrite /is_blackout => -> //=; rewrite andbT andbF //. }
+      { move: (SUP); rewrite /is_blackout => ->; rewrite andTb //=.
+        have L : forall (a b : bool), a || b <= a + b by clear => [] [] [].
+        by apply L. }
+    Qed.
+
+    (** In this section, we prove that the (abstract) cumulative
+        interfering workload due to other higher-or-equal priority
+        jobs is equal to the conventional workload (from other
+        higher-or-equal priority jobs). *)
+    Section InstantiatedWorkloadEquivalence.
+
+      (** Let <<[t1, t2)>> be any time interval. *)
+      Variables t1 t2 : instant.
+
+      (** Consider any job [j] of [tsk]. *)
+      Variable j : Job.
+      Hypothesis H_j_arrives : arrives_in arr_seq j.
+      Hypothesis H_job_of_tsk : job_of_task tsk j.
+
+      (** The cumulative interfering workload (w.r.t. [j]) due to
+          other higher-or-equal priority jobs is equal to the
+          conventional workload from other higher-or-equal priority
+          jobs. *)
+      Lemma cumulative_iw_hep_eq_workload_of_ohep :
+        cumulative_other_hep_jobs_interfering_workload arr_seq j t1 t2
+        = workload_of_other_hep_jobs arr_seq j t1 t2.
+      Proof.
+        rewrite /cumulative_other_hep_jobs_interfering_workload /workload_of_other_hep_jobs.
+        case NEQ: (t1 < t2); last first.
+        { move: NEQ => /negP /negP; rewrite -leqNgt; move => NEQ.
+          rewrite big_geq // /arrivals_between big_geq //.
+          by rewrite /workload_of_jobs big_nil. }
+        { interval_to_duration t1 t2 k.
+          elim: k => [|k IHk].
+          - rewrite !addn0 big_geq// /arrivals_between big_geq//.
+            by rewrite /workload_of_jobs big_nil.
+          - rewrite addnS big_nat_recr //=; last by rewrite leq_addr.
+            rewrite IHk /arrivals_between big_nat_recr //=.
+            + by rewrite /workload_of_jobs big_cat.
+            + by rewrite leq_addr. }
+      Qed.
+
+    End InstantiatedWorkloadEquivalence.
+
+    (** In this section we prove that the abstract definition of busy
+        interval is equivalent to the conventional, concrete
+        definition of busy interval for JLFP scheduling. *)
+    Section BusyIntervalEquivalence.
+
+      (** In order to avoid confusion, we denote the notion of a quiet
+          time in the _classical_ sense as [quiet_time_cl], and the
+          notion of quiet time in the _abstract_ sense as
+          [quiet_time_ab]. *)
+      Let quiet_time_cl := classical.quiet_time arr_seq sched.
+      Let quiet_time_ab := abstract.definitions.quiet_time sched.
+
+      (** Same for the two notions of a busy interval prefix ... *)
+      Let busy_interval_prefix_cl := classical.busy_interval_prefix arr_seq sched.
+      Let busy_interval_prefix_ab := abstract.definitions.busy_interval_prefix sched.
+
+      (** ... and the two notions of a busy interval. *)
+      Let busy_interval_cl := classical.busy_interval arr_seq sched.
+      Let busy_interval_ab := abstract.definitions.busy_interval sched.
+
+      (** Consider any job [j] of [tsk]. *)
+      Variable j : Job.
+      Hypothesis H_j_arrives : arrives_in arr_seq j.
+
+      (** To show the equivalence of the notions of busy intervals, we
+          first show that the notions of quiet time are also
+          equivalent. *)
+
+      (** First, we show that the classical notion of quiet time
+          implies the abstract notion of quiet time. *)
+      Lemma quiet_time_cl_implies_quiet_time_ab :
+        forall t, quiet_time_cl j t -> quiet_time_ab j t.
+      Proof.
+        have zero_is_quiet_time: forall j, quiet_time_cl j 0.
+        { by move => jhp ARR HP AB; move: AB; rewrite /arrived_before ltn0. }
+        move=> t QT; apply/andP; split; last first.
+        { rewrite negb_and negbK; apply/orP.
+          by case ARR: (arrived_before j t); [right | left]; [apply QT | ]. }
+        { erewrite cumulative_interference_split, cumulative_interfering_workload_split; rewrite eqn_add2l.
+          rewrite cumulative_i_ohep_eq_service_of_ohep //.
+          rewrite //= cumulative_iw_hep_eq_workload_of_ohep eq_sym; apply/eqP.
+          apply all_jobs_have_completed_equiv_workload_eq_service => //.
+          move => j0 IN HEP; apply QT.
+          - by apply in_arrivals_implies_arrived in IN.
+          - by move: HEP => /andP [HEP HP].
+          - by apply in_arrivals_implies_arrived_between in IN.
+        }
+      Qed.
+
+      (** And vice versa, the abstract notion of quiet time implies
+          the classical notion of quiet time. *)
+      Lemma quiet_time_ab_implies_quiet_time_cl :
+        forall t, quiet_time_ab j t -> quiet_time_cl j t.
+      Proof.
+        have zero_is_quiet_time: forall j, quiet_time_cl j 0.
+        { by move => jhp ARR HP AB; move: AB; rewrite /arrived_before ltn0. }
+        move => t /andP [T0 T1] jhp ARR HP ARB.
+        eapply all_jobs_have_completed_equiv_workload_eq_service with
+          (P := fun jhp => hep_job jhp j) (t1 := 0) (t2 := t) => //.
+        erewrite service_of_jobs_case_on_pred with (P2 := fun j' => j' != j).
+        erewrite workload_of_jobs_case_on_pred with (P' := fun j' => j' != j) => //.
+        replace ((fun j0 : Job => hep_job j0 j && (j0 != j))) with (another_hep_job^~j); last by rewrite /another_hep_job.
+        rewrite -/(service_of_other_hep_jobs arr_seq sched j 0 t) -cumulative_i_ohep_eq_service_of_ohep //.
+        rewrite -/(workload_of_other_hep_jobs arr_seq j 0 t) -cumulative_iw_hep_eq_workload_of_ohep //.
+        move: T1; rewrite negb_and => /orP [NA | /negPn COMP].
+        { have PRED__eq: {in arrivals_between arr_seq 0 t, (fun j__copy : Job => hep_job j__copy j && ~~ (j__copy != j)) =1 pred0}.
+          { move => j__copy IN; apply negbTE.
+            rewrite negb_and; apply/orP; right; apply/negPn/eqP => EQ; subst j__copy.
+            move: NA => /negP CONTR; apply: CONTR.
+            by apply in_arrivals_implies_arrived_between in IN. }
+          erewrite service_of_jobs_equiv_pred with (P2 := pred0) => [|//].
+          erewrite workload_of_jobs_equiv_pred with (P' := pred0) => [|//].
+          move: T0; erewrite cumulative_interference_split, cumulative_interfering_workload_split; rewrite eqn_add2l => /eqP EQ.
+          rewrite EQ; clear EQ; apply/eqP; rewrite eqn_add2l.
+          by erewrite workload_of_jobs_pred0, service_of_jobs_pred0.
+        }
+        { have PRED__eq: {in arrivals_between arr_seq 0 t, (fun j0 : Job => hep_job j0 j && ~~ (j0 != j)) =1 eq_op j}.
+          { move => j__copy IN.
+            replace (~~ (j__copy != j)) with (j__copy == j); last by case: (j__copy == j).
+            rewrite eq_sym; destruct (j == j__copy) eqn:EQ; last by rewrite Bool.andb_false_r.
+            by move: EQ => /eqP EQ; rewrite Bool.andb_true_r; apply/eqP; rewrite eqb_id; subst. }
+          erewrite service_of_jobs_equiv_pred with (P2 := eq_op j) => [|//].
+          erewrite workload_of_jobs_equiv_pred with (P' := eq_op j) => [|//].
+          move: T0; erewrite cumulative_interference_split, cumulative_interfering_workload_split; rewrite eqn_add2l => /eqP EQ.
+          rewrite EQ; clear EQ; apply/eqP; rewrite eqn_add2l.
+          apply/eqP; eapply all_jobs_have_completed_equiv_workload_eq_service with
+            (P := eq_op j) (t1 := 0) (t2 := t) => //.
+          { by move => j__copy _ /eqP EQ; subst j__copy. }
+        }
+      Qed.
+
+      (** The equivalence trivially follows from the lemmas above. *)
+      Corollary instantiated_quiet_time_equivalent_quiet_time :
+        forall t,
+          quiet_time_cl j t <-> quiet_time_ab j t.
+      Proof.
+        move => ?; split.
+        - by apply quiet_time_cl_implies_quiet_time_ab.
+        - by apply quiet_time_ab_implies_quiet_time_cl.
+      Qed.
+
+      (** Based on that, we prove that the concept of a busy-interval
+          prefix obtained by instantiating the abstract definition of
+          busy-interval prefix coincides with the conventional
+          definition of busy-interval prefix. *)
+      Lemma instantiated_busy_interval_prefix_equivalent_busy_interval_prefix :
+        forall t1 t2, busy_interval_prefix_cl j t1 t2 <-> busy_interval_prefix_ab j t1 t2.
+      Proof.
+        move => t1 t2; split.
+        { move => [NEQ [QTt1 [NQT REL]]].
+          split=> [//|]; split.
+          - by apply instantiated_quiet_time_equivalent_quiet_time in QTt1.
+          - by move => t NE QT; eapply NQT; eauto 2; apply instantiated_quiet_time_equivalent_quiet_time.
+        }
+        { move => [/andP [NEQ1 NEQ2] [QTt1 NQT]].
+          split; [ | split; [ |split] ].
+          - by apply leq_ltn_trans with (job_arrival j).
+          - by eapply instantiated_quiet_time_equivalent_quiet_time.
+          - by move => t NEQ QT; eapply NQT; eauto 2; eapply instantiated_quiet_time_equivalent_quiet_time in QT.
+          - by apply/andP.
+        }
+      Qed.
+
+      (** Similarly, we prove that the concept of busy interval
+          obtained by instantiating the abstract definition of busy
+          interval coincides with the conventional definition of busy
+          interval. *)
+      Lemma instantiated_busy_interval_equivalent_busy_interval :
+        forall t1 t2, busy_interval_cl j t1 t2 <-> busy_interval_ab j t1 t2.
+      Proof.
+        move => t1 t2; split.
+        { move => [PREF QTt2]; split.
+          - by apply instantiated_busy_interval_prefix_equivalent_busy_interval_prefix.
+          - by eapply instantiated_quiet_time_equivalent_quiet_time in QTt2.
+        }
+        { move => [PREF QTt2]; split.
+          - by apply instantiated_busy_interval_prefix_equivalent_busy_interval_prefix.
+          - by eapply instantiated_quiet_time_equivalent_quiet_time.
+        }
+      Qed.
+
+      (** For the sake of proof automation, we note the frequently needed
+          special case of an abstract busy window implying the existence of a
+          classic quiet time. *)
+      Fact abstract_busy_interval_classic_quiet_time :
+        forall t1 t2,
+          busy_interval_ab j t1 t2 -> quiet_time_cl j t1.
+      Proof.
+        by move=> ? ? /instantiated_busy_interval_equivalent_busy_interval [[_ [? _]] _].
+      Qed.
+
+      (** Also for automation, we note a similar fact about classic busy-window prefixes. *)
+      Fact abstract_busy_interval_classic_busy_interval_prefix :
+        forall t1 t2,
+          busy_interval_ab j t1 t2 -> busy_interval_prefix_cl j t1 t2.
+      Proof. by move=> ? ? /instantiated_busy_interval_equivalent_busy_interval [+ _]. Qed.
+
+    End BusyIntervalEquivalence.
+
+  End Equivalences.
+
+  (** In this section we prove some properties about the interference
+      and interfering workload as defined in this file. *)
+  Section I_IW_correctness.
+
+    (** Consider work-bearing readiness. *)
+    Context `{!JobReady Job PState}.
+    Hypothesis H_work_bearing_readiness : work_bearing_readiness arr_seq sched.
+
+    (** Assume that the schedule is valid and work-conserving. *)
+    Hypothesis H_sched_valid : valid_schedule sched arr_seq.
+
+    (** Note that we differentiate between abstract and classical
+        notions of work-conserving schedule ... *)
+    Let work_conserving_ab := definitions.work_conserving arr_seq sched.
+    Let work_conserving_cl := work_conserving.work_conserving arr_seq sched.
+
+    (** ... as well as notions of busy interval prefix. *)
+    Let busy_interval_prefix_ab := definitions.busy_interval_prefix sched.
+    Let busy_interval_prefix_cl := classical.busy_interval_prefix arr_seq sched.
+
+    (** We assume that the schedule is a work-conserving schedule in
+        the _classical_ sense, and later prove that the hypothesis
+        about abstract work-conservation also holds. *)
+    Hypothesis H_work_conserving : work_conserving_cl.
+
+    (** In this section, we prove the correctness of interference
+        inside the busy interval, i.e., we prove that if interference
+        for a job is [false] then the job is scheduled and vice versa.
+        This property is referred to as abstract work conservation. *)
+    Section Abstract_Work_Conservation.
+
+      (** Consider a job [j] that is in the arrival sequence
+          and has a positive job cost. *)
+      Variable j : Job.
+      Hypothesis H_arrives : arrives_in arr_seq j.
+      Hypothesis H_job_cost_positive : 0 < job_cost j.
+
+      (** Let the busy interval of the job be <<[t1, t2)>>. *)
+      Variable t1 t2 : instant.
+      Hypothesis H_busy_interval_prefix : busy_interval_prefix_ab j t1 t2.
+
+      (** Consider a time [t] inside the busy interval of the job. *)
+      Variable t : instant.
+      Hypothesis H_t_in_busy_interval : t1 <= t < t2.
+
+      (** First, we note that, similarly to the ideal uni-processor
+          case, there is no idle time inside of a busy interval. That
+          is, there is a job scheduled at time [t]. *)
+      Local Lemma busy_implies_not_idle :
+        exists j, scheduled_at sched j t.
+      Proof.
+        have [IDLE|[s SCHEDs]] := scheduled_at_cases arr_seq ltac:(eauto) sched ltac:(eauto) ltac:(eauto) t; last by (exists s).
+        exfalso; eapply instant_t_is_not_idle in IDLE => //.
+        by apply instantiated_busy_interval_prefix_equivalent_busy_interval_prefix.
+      Qed.
+
+      (** We then prove that if interference is [false] at a time [t]
+          then the job is scheduled. *)
+      Lemma not_interference_implies_scheduled :
+        ~~ interference j t -> receives_service_at sched j t.
+      Proof.
+        rewrite !negb_or /another_hep_job_interference => /andP [/andP [HYP1 HYP2] /hasPn HYP3].        
+        move: HYP1; rewrite /is_blackout negbK => SUP; apply ideal_progress_inside_supplies => //.
+        move: HYP2; rewrite negb_and negbK => /orP [SERV | /hasPn SI].
+        { by apply service_at_implies_scheduled_at; apply: served_at_and_receives_service_consistent => //. }
+        move: busy_implies_not_idle => [jo SCHED].
+        have RSERV : receives_service_at sched jo t by apply ideal_progress_inside_supplies.
+        have INRSERV : jo \in served_jobs_at arr_seq sched t by apply receives_service_and_served_at_consistent.
+        move: (HYP3 _ INRSERV); rewrite negb_and => /orP [LP | EQ]; last first.
+        - by move: EQ; rewrite negbK => /eqP EQ; subst jo.
+        - by move: (SI _ INRSERV); rewrite LP.
+      Qed.
+
+      (** Conversely, if the job is scheduled at [t] then interference is [false]. *)
+      Lemma scheduled_implies_no_interference :
+        receives_service_at sched j t -> ~~ interference j t.
+      Proof.
+        move=> RSERV. apply/negP => /orP [/orP[BL|PINV] | INT].
+        - by apply/negP; first apply: no_blackout_when_service_received.
+        - by apply/negP; first apply: receives_service_implies_no_service_inversion.
+        - move: INT; rewrite_neg @no_ahep_interference_when_served.
+          by apply: receives_service_implies_has_supply.
+      Qed.
+
+    End Abstract_Work_Conservation.
+
+    (** Using the above two lemmas, we can prove that abstract work
+        conservation always holds for these instantiations of
+        interference (I) and interfering workload (W). *)
+    Corollary instantiated_i_and_w_are_coherent_with_schedule :
+      work_conserving_ab.
+    Proof.
+      move => j t1 t2 t ARR POS BUSY NEQ; split.
+      - by move=> G; apply: (not_interference_implies_scheduled j ARR POS); eauto 2; apply/negP.
+      - by move=> SERV; apply/negP; apply: scheduled_implies_no_interference; eauto 2.
+    Qed.
+
+    (** Next, in order to prove that these definitions of interference
+        and interfering workload are consistent with sequential tasks,
+        we need to assume that the policy under consideration respects
+        sequential tasks. *)
+    Hypothesis H_policy_respects_sequential_tasks : policy_respects_sequential_tasks JLFP.
+
+    (** We prove that these definitions of interference and
+        interfering workload are consistent with sequential tasks. *)
+    Lemma instantiated_interference_and_workload_consistent_with_sequential_tasks :
+      interference_and_workload_consistent_with_sequential_tasks arr_seq sched tsk.
+    Proof.
+      move => j t1 t2 ARR /eqP TSK POS BUSY.
+      eapply instantiated_busy_interval_equivalent_busy_interval in BUSY => //.
+      eapply all_jobs_have_completed_equiv_workload_eq_service => //.
+      move => s INs /eqP TSKs.
+      move: (INs) => NEQ.
+      eapply in_arrivals_implies_arrived_between in NEQ => //.
+      move: NEQ => /andP [_ JAs].
+      move: (BUSY) => [[ _ [QT [_ /andP [JAj _]]] _]].
+      apply QT => //; first exact: in_arrivals_implies_arrived.
+      apply H_policy_respects_sequential_tasks; first by rewrite  TSK TSKs.
+      by apply leq_trans with t1; [lia |].
+    Qed.
+
+    (** Finally, we show that cumulative interference (I) never exceeds
+        cumulative interfering workload (W). *)
+    Lemma instantiated_i_and_w_no_speculative_execution :
+      no_speculative_execution.
+    Proof.
+      move=> j t1.
+      rewrite cumulative_interference_split cumulative_interfering_workload_split.
+      rewrite leq_add2l cumulative_i_ohep_eq_service_of_ohep //=.
+      rewrite cumulative_iw_hep_eq_workload_of_ohep.
+      by apply service_of_jobs_le_workload => //.
+    Qed.
+
+  End I_IW_correctness.
+
+End JLFPInstantiation.

analysis/abstract/restricted_supply/search_space/edf.v

+Require Export prosa.analysis.facts.model.rbf.
+Require Export prosa.analysis.abstract.search_space.
+Require Export prosa.analysis.definitions.blocking_bound.edf.
+Require Export prosa.analysis.facts.workload.edf_athep_bound.
+
+(** * Abstract Search Space is a Subset of Restricted Supply EDF Search Space *)
+
+(** A response-time analysis usually involves solving the
+    response-time equation for various relative arrival times
+    (w.r.t. the beginning of the corresponding busy interval) of a job
+    under analysis. To reduce the time complexity of the analysis, the
+    state of the art uses the notion of a search space. Intuitively,
+    this corresponds to all "interesting" arrival offsets that the job
+    under analysis might have with regard to the beginning of its busy
+    window.
+
+    In this file, we prove that the search space derived from the aRSA
+    theorem is a subset of the search space for the EDF scheduling
+    policy with restricted supply. In other words, by solving the
+    response-time equation for points in the EDF search space, one
+    also checks all points in the aRTA search space, which makes EDF
+    compatible with aRTA w.r.t. the search space. *)
+Section SearchSpaceSubset.
+
+  (** Consider any type of tasks. *)
+  Context {Task : TaskType}.
+  Context `{TaskCost Task}.
+  Context `{TaskDeadline Task}.
+  Context `{TaskMaxNonpreemptiveSegment Task}.
+
+  (** Consider an arbitrary task set [ts]. *)
+  Variable ts : seq Task.
+
+  (** Let [max_arrivals] be a family of valid arrival curves. *)
+  Context `{MaxArrivals Task}.
+  Hypothesis H_valid_arrival_curve :
+    valid_taskset_arrival_curve ts max_arrivals.
+
+  (** Let [tsk] be any task in [ts] that is to be analyzed. *)
+  Variable tsk : Task.
+  Hypothesis H_tsk_in_ts : tsk \in ts.
+
+  (** Let [L] be an arbitrary positive constant. Normally, [L] denotes
+      an upper bound on the length of a busy interval of a job of
+      [tsk]. In this file, however, [L] can be any positive
+      constant. *)
+  Variable L : duration.
+  Hypothesis H_L_positive : 0 < L.
+
+  (** For brevity, let's denote the relative deadline of a task as D. *)
+  Let D tsk := task_deadline tsk.
+
+  (** We introduce [rbf] as an abbreviation of the task request bound function. *)
+  Let rbf := task_request_bound_function.
+
+  (** To reduce the time complexity of the analysis, we introduce the
+      notion of a search space for EDF. Intuitively, this corresponds
+      to all "interesting" arrival offsets that the job under analysis
+      might have with regard to the beginning of its busy window. *)
+
+  (** In the case of the search space for EDF, we consider three
+      conditions. First, we ask whether [task_rbf A ≠ task_rbf (A +
+      ε)]. *)
+  Let task_rbf_changes_at (A : duration) :=
+    rbf tsk A != rbf tsk (A + ε).
+
+  (** Second, we ask whether there exists a task [tsko] from [ts] such
+      that [tsko ≠ tsk] and [rbf(tsko, A + D tsk - D tsko) ≠ rbf(tsko,
+      A + ε + D tsk - D tsko)]. *)
+  Let bound_on_total_hep_workload_changes_at (A : duration) :=
+    let new_hep_job_released_by tsko :=
+      (tsk != tsko) && (rbf tsko (A + D tsk - D tsko) != rbf tsko ((A + ε) + D tsk - D tsko))
+    in has new_hep_job_released_by ts.
+
+  (** Third, we ask whether [blocking_bound (A - ε) ≠ blocking_bound A]. *)
+  Let blocking_bound_changes_at (A : duration) :=
+    blocking_bound ts tsk (A - ε) != blocking_bound ts tsk A.
+
+  (** The final search space for EDF is the set of offsets less
+      than [L] and where [priority_inversion_bound], [task_rbf], or
+      [bound_on_total_hep_workload] changes in value. *)
+  Definition is_in_search_space (A : duration) :=
+    (A < L) && (blocking_bound_changes_at A
+                || task_rbf_changes_at A
+                || bound_on_total_hep_workload_changes_at A).
+
+  (** To rule out pathological cases with the search space, we assume
+      that the task cost is positive and the arrival curve is
+      non-pathological. *)
+  Hypothesis H_task_cost_pos : 0 < task_cost tsk.
+  Hypothesis H_arrival_curve_pos : 0 < max_arrivals tsk ε.
+
+  (** For brevity, let us introduce a shorthand for an intra-IBF. The
+      abstract search space is derived via intra-IBF. *)
+  Let intra_IBF (A F : duration) :=
+    rbf tsk (A + ε) - task_cost tsk
+    + (blocking_bound ts tsk A + bound_on_athep_workload ts tsk A F).
+
+  (** Then, abstract RTA's standard search space is a subset of the
+      computation-oriented version defined above. *)
+  Lemma search_space_sub :
+    forall A,
+      abstract.search_space.is_in_search_space L intra_IBF A ->
+      is_in_search_space A.
+  Proof.
+    move => A [-> | [/andP [POSA LTL] [x [LTx INSP2]]]]; apply/andP; split => //.
+    { apply/orP; left; apply/orP; right.
+      rewrite /task_rbf_changes_at /rbf task_rbf_0_zero // eq_sym -lt0n add0n.
+      by apply task_rbf_epsilon_gt_0 => //.
+    }
+    { apply contraT; rewrite !negb_or => /andP [/andP [/negPn/eqP PI /negPn/eqP RBF]  WL].
+      exfalso; apply INSP2.
+      rewrite /intra_IBF subnK // RBF.
+      apply /eqP; rewrite eqn_add2l PI eqn_add2l.
+      rewrite /bound_on_athep_workload subnK //.
+      apply /eqP; rewrite big_seq_cond [RHS]big_seq_cond.
+      apply eq_big => // tsk_i /andP [TS OTHER].
+      move: WL; rewrite /bound_on_total_hep_workload_changes_at /D => /hasPn WL.
+      move: {WL} (WL tsk_i TS) =>  /nandP [/negPn/eqP EQ|/negPn/eqP WL];
+                                  first by move: OTHER; rewrite EQ => /neqP.
+      case: (ltngtP (A + ε + task_deadline tsk - task_deadline tsk_i) x) => [ltn_x|gtn_x|eq_x]; rewrite /minn.
+      { by rewrite ifT //; lia. }
+      { rewrite ifF //.
+        by move: gtn_x; rewrite leq_eqVlt  => /orP [/eqP EQ|LEQ]; lia. }
+      { case: (A + task_deadline tsk - task_deadline tsk_i < x).
+        - by rewrite -/rbf WL.
+        - by rewrite eq_x. } }
+  Qed.
+
+End SearchSpaceSubset.

analysis/abstract/restricted_supply/search_space/elf.v

+Require Export prosa.analysis.facts.model.rbf.
+Require Export prosa.analysis.abstract.search_space.
+Require Export prosa.analysis.definitions.blocking_bound.elf.
+Require Export prosa.analysis.facts.workload.elf_athep_bound.
+
+(** * Abstract Search Space is a Subset of Restricted Supply ELF Search Space *)
+Section SearchSpaceSubset.
+
+  (** Consider any type of tasks with relative priority points. *)
+  Context {Task : TaskType}.
+  Context `{TaskCost Task}.
+  Context `{TaskDeadline Task}.
+  Context `{TaskMaxNonpreemptiveSegment Task}.
+  Context `{PriorityPoint Task}.
+
+  (** Consider an arbitrary task set [ts]. *)
+  Variable ts : seq Task.
+
+  (** Let [max_arrivals] be a family of valid arrival curves. *)
+  Context `{MaxArrivals Task}.
+  Hypothesis H_valid_arrival_curve :
+    valid_taskset_arrival_curve ts max_arrivals.
+
+  (** Consider any FP policy. *)
+  Context {FP : FP_policy Task}.
+
+  (** Let [tsk] be any task in [ts] that is to be analyzed. *)
+  Variable tsk : Task.
+  Hypothesis H_tsk_in_ts : tsk \in ts.
+
+  (** Let [L] be an arbitrary positive constant. Normally, [L] denotes
+      an upper bound on the length of a busy interval of a job of
+      [tsk]. In this file, however, [L] can be any positive
+      constant. *)
+  Variable L : duration.
+  Hypothesis H_L_positive : 0 < L.
+
+  (** We introduce [task_rbf] as an abbreviation of the task request bound function. *)
+  Let task_rbf := task_request_bound_function tsk.
+
+  (** To reduce the time complexity of the analysis, we introduce the
+      notion of a search space for ELF. Intuitively, this corresponds
+      to all "interesting" arrival offsets that the job under analysis
+      might have with regard to the beginning of its busy window. *)
+
+  (** In the case of the search space for ELF, we consider three
+      conditions.
+
+      First, we ask whether [rbf A ≠ rbf (A + ε)]. *)
+  Let task_rbf_changes_at (A : duration) :=
+    task_rbf A != task_rbf (A + ε).
+
+  (** Second, we limit our search space to those arrival offsets where
+      the bound on higher-or-equal priority workload changes in value.
+
+      Since the bound on workload from higher priority task does not depend
+      on the arrival offset [A], we are only concerned about the workload from
+      equal priority tasks.
+      For this, we ask whether there exists a task [tsko ≠ tsk] in task set [ts]
+      such that
+     [ep_task_interfering_interval_length tsk tsko (A - ε) != ep_task_interfering_interval_length tsk tsko A]. *)
+  Let bound_on_ep_task_workload_changes_at (A : duration) :=
+    let new_hep_job_released_by tsko :=
+      (ep_task tsk tsko) && (tsko != tsk)
+      && (ep_task_interfering_interval_length tsk tsko (A - ε) != ep_task_interfering_interval_length tsk tsko A)
+    in has new_hep_job_released_by ts.
+
+  (** Third, we ask whether [blocking_bound (A - ε) ≠ blocking_bound A]. *)
+  Let blocking_bound_changes_at (A : duration) :=
+    blocking_bound ts tsk (A - ε) != blocking_bound ts tsk A.
+
+  (** The final search space for ELF is the set of offsets less
+      than [L] and where [task_rbf], [blocking_bound] or
+      [bound_on_ep_task_workload] changes in value. *)
+  Definition is_in_search_space (A : duration) :=
+    (A < L) && (blocking_bound_changes_at A
+                || task_rbf_changes_at A
+                || bound_on_ep_task_workload_changes_at A).
+
+  (** To rule out pathological cases with the search space, we assume
+      that the task cost is positive and the arrival curve is
+      non-pathological. *)
+  Hypothesis H_task_cost_pos : 0 < task_cost tsk.
+  Hypothesis H_arrival_curve_pos : 0 < max_arrivals tsk ε.
+
+  (** For brevity, let us introduce a shorthand for an intra-IBF. The
+      abstract search space is derived via intra-IBF. *)
+  Let intra_IBF (A F : duration) :=
+    task_rbf (A + ε) - task_cost tsk
+    + (blocking_bound ts tsk A + bound_on_athep_workload ts tsk A F).
+
+  (** Then, abstract RTA's standard search space is a subset of the
+      computation-oriented version defined above. *)
+  Lemma search_space_sub :
+    forall A,
+      abstract.search_space.is_in_search_space L intra_IBF A ->
+      is_in_search_space A.
+  Proof.
+    move => A [-> | [/andP [POSA LTL] [x [LTx INSP2]]]]; apply/andP; split => //.
+    { apply/orP; left; apply/orP; right.
+      rewrite /task_rbf_changes_at /task_rbf task_rbf_0_zero //=.
+      { rewrite eq_sym -lt0n add0n.
+        by apply task_rbf_epsilon_gt_0 => //. } }
+    { apply contraT; rewrite !negb_or => /andP [/andP [/negPn/eqP PI /negPn/eqP RBF]  WL].
+      exfalso; apply INSP2.
+      rewrite /intra_IBF subnK // RBF.
+      apply /eqP; rewrite eqn_add2l PI eqn_add2l.
+      rewrite /bound_on_athep_workload /bound_on_ep_task_workload /bound_on_hp_task_workload /ep_task_interfering_interval_length.
+      rewrite subnK //.
+      rewrite eqn_add2l.
+      apply /eqP; rewrite big_seq_cond [RHS]big_seq_cond.
+      apply eq_big => // tsk_i /andP [TS OTHER].
+      move: WL.
+      rewrite /bound_on_ep_task_workload_changes_at /ep_task_interfering_interval_length => /hasPn WL.
+      move: {WL} (WL tsk_i TS) =>  /nandP [/negbTE EQ|/negPn/eqP WL].
+      { by move: OTHER; rewrite EQ. }
+      have [leq_x|gtn_x] := leqP `|Num.max 0%R (ep_task_interfering_interval_length tsk tsk_i A)| x.
+      { move: WL.
+        rewrite subnK // /task_rbf => WL.
+        by rewrite WL (minn_idPl leq_x). }
+      move: WL.
+      rewrite subnK // /task_rbf => WL.
+      by rewrite WL (minn_idPr (ltnW gtn_x)). }
+  Qed.
+
+End SearchSpaceSubset.

analysis/abstract/restricted_supply/search_space/fifo.v

+Require Export prosa.analysis.facts.model.rbf.
+Require Export prosa.analysis.abstract.search_space.
+Require Import prosa.analysis.facts.priority.fifo.
+Require Import prosa.analysis.definitions.sbf.pred.
+
+(** * The Abstract Search Space is a Subset of the FIFO Search Space *)
+
+(** A response-time analysis usually involves solving the
+    response-time equation for various relative arrival times
+    (w.r.t. the beginning of the corresponding busy interval) of a job
+    under analysis. To reduce the time complexity of the analysis, the
+    state of the art uses the notion of a search space. Intuitively,
+    this corresponds to all "interesting" arrival offsets that the job
+    under analysis might have with regard to the beginning of its busy
+    window.
+
+    In this file, we prove that the search space derived from the aRTA
+    theorem is a subset of the search space for the FIFO scheduling
+    policy with restricted supply. In other words, by solving the
+    response-time equation for points in the FIFO search space, one also
+    checks all points in the aRTA search space, which makes FIFO
+    compatible with aRTA w.r.t. the search space. *)
+Section SearchSpaceSubset.
+
+  (** Consider a restricted-supply uniprocessor model where the
+      minimum amount of supply is defined via a monotone
+      unit-supply-bound function [SBF]. *)
+  Context {SBF : SupplyBoundFunction}.
+
+  (** Consider any type of tasks. *)
+  Context {Task : TaskType}.
+  Context `{TaskCost Task}.
+
+  (** Consider an arbitrary task set [ts]. *)
+  Variable ts : seq Task.
+
+  (** 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.
+
+  (** For brevity, let's denote the request-bound function of a task
+      as [rbf]. *)
+  Let rbf tsk := task_request_bound_function tsk.
+
+  (** Let [L] be an arbitrary positive constant. Typically, [L]
+      denotes an upper bound on the length of a busy interval of a job
+      of [tsk]. In this file, however, [L] can be any positive
+      constant. *)
+  Variable L : duration.
+  Hypothesis H_L_positive : 0 < L.
+
+  (** In the case of [FIFO], the concrete search space is the set of
+      offsets less than [L] such that there exists a task [tsk] in
+      [ts] such that [rbf tsk (A) ≠ rbf tsk (A + ε)]. *)
+  Definition is_in_search_space (A : duration) :=
+    let rbf_makes_a_step tsk := rbf tsk A != rbf tsk (A + ε) in
+    (A < L) && has rbf_makes_a_step ts.
+
+  (** Let [tsk] be any task in [ts] that is to be analyzed. *)
+  Variable tsk : Task.
+  Hypothesis H_tsk_in_ts : tsk \in ts.
+
+  (** To rule out pathological cases with the search space, we assume
+      that the task cost is positive and the arrival curve is
+      non-pathological. *)
+  Hypothesis H_task_cost_pos : 0 < task_cost tsk.
+  Hypothesis H_arrival_curve_pos : 0 < max_arrivals tsk ε.
+
+  (** For brevity, let us introduce a shorthand for an IBF (used by
+      aRTA). The abstract search space is derived via IBF. *)
+  Local Definition IBF (A F : duration) :=
+    (F - SBF F) + (total_request_bound_function ts (A + ε) - task_cost tsk).
+
+  (** Then, abstract RTA's standard search space is a subset of the
+      computation-oriented version defined above. *)
+  Lemma search_space_sub :
+    forall A,
+      abstract.search_space.is_in_search_space L IBF A ->
+      is_in_search_space A.
+  Proof.
+    move => A [INSP | [/andP [POSA LTL] [x [LTx INSP2]]]].
+    { subst A.
+      apply/andP; split=> [//|].
+      apply /hasP; exists tsk => [//|].
+      rewrite neq_ltn; apply/orP; left.
+      rewrite /rbf task_rbf_0_zero // add0n.
+      by apply task_rbf_epsilon_gt_0 => //.
+    }
+    { apply /andP; split=> [//|].
+      apply /hasPn => EQ2.
+      rewrite /IBF in INSP2; rewrite /total_request_bound_function.
+      rewrite subnK in INSP2 => //.
+      apply INSP2; clear INSP2.
+      have ->// : total_request_bound_function ts A = total_request_bound_function ts (A + ε).
+      apply eq_big_seq => //= task IN.
+      by move: (EQ2 task IN) => /negPn /eqP. }
+  Qed.
+
+End SearchSpaceSubset.

analysis/abstract/restricted_supply/search_space/fifo_fixpoint.v

+Require Export prosa.model.priority.fifo.
+Require Export prosa.model.task.preemption.parameters.
+Require Export prosa.analysis.definitions.sbf.busy.
+Require Export prosa.analysis.abstract.restricted_supply.search_space.fifo.
+
+(** * Concrete to Abstract Fixpoint Reduction *)
+
+(** In this file, we show that a solution to a concrete fixpoint
+    equation under the FIFO policy implies a solution to the
+    abstract fixpoint equation required by aRSA. *)
+Section ConcreteToAbstractFixpointReduction.
+
+  (** Consider any type of tasks, each characterized by a WCET
+      [task_cost], an arrival curve [max_arrivals], a
+      run-to-completion threshold [task_rtct], and a bound on the
+      task's maximum non-preemptive segment
+      [task_max_nonpreemptive_segment] ... *)
+  Context {Task : TaskType}.
+  Context `{TaskCost Task}.
+  Context `{MaxArrivals Task}.
+  Context `{TaskRunToCompletionThreshold Task}.
+  Context `{TaskMaxNonpreemptiveSegment Task}.
+
+  (** ... and any type of jobs associated with these tasks, where each
+      job has a task [job_task], a cost [job_cost], an arrival time
+      [job_arrival], and a predicate indicating when the job is
+      preemptable [job_preemptable]. *)
+  Context {Job : JobType}.
+  Context `{JobTask Job Task}.
+  Context `{JobCost Job}.
+  Context `{JobArrival Job}.
+  Context `{JobPreemptable Job}.
+
+  (** Consider any processor model ... *)
+  Context `{PState : ProcessorState Job}.
+
+  (** ... where the minimum amount of supply is defined via a monotone
+      unit-supply-bound function [SBF]. *)
+  Context {SBF : SupplyBoundFunction}.
+  Hypothesis H_SBF_monotone : sbf_is_monotone SBF.
+  Hypothesis H_unit_SBF : unit_supply_bound_function SBF.
+
+  (** We consider an arbitrary task set [ts]. *)
+  Variable ts : seq Task.
+
+  (** Let [tsk] be any task in [ts] that is to be analyzed. *)
+  Variable tsk : Task.
+  Hypothesis H_tsk_in_ts : tsk \in ts.
+
+  (** Consider any arrival sequence ... *)
+  Variable arr_seq : arrival_sequence Job.
+
+  (** ... and assume that [max_arrivals] defines a valid arrival curve
+      for each task. *)
+  Hypothesis H_valid_arrival_curve : valid_taskset_arrival_curve ts max_arrivals.
+
+  (** Consider any schedule. *)
+  Variable sched : schedule PState.
+
+  (** Next, we assume that [SBF] properly characterizes all busy
+      intervals (w.r.t. task [tsk]) in [sched]. That is, (1) [SBF 0 =
+      0] and (2) for any duration [Δ], at least [SBF Δ] supply is
+      available in any busy-interval prefix of length [Δ]. *)
+  Hypothesis H_valid_SBF : valid_busy_sbf arr_seq sched tsk SBF.
+
+  (** We assume that [tsk] is described by a valid task
+      run-to-completion threshold_ *)
+  Hypothesis H_valid_run_to_completion_threshold :
+    valid_task_run_to_completion_threshold arr_seq tsk.
+
+  (** Let [L] be an arbitrary positive constant. Typically, [L]
+      denotes an upper bound on the length of a busy interval of a job
+      of [tsk]. In this file, however, [L] can be any positive
+      constant. *)
+  Variable L : duration.
+  Hypothesis H_L_positive : 0 < L.
+
+  (** To rule out pathological cases with the search space, we assume
+      that the task cost is positive and the arrival curve is
+      non-pathological. *)
+  Hypothesis H_task_cost_pos : 0 < task_cost tsk.
+  Hypothesis H_arrival_curve_pos : 0 < max_arrivals tsk ε.
+
+  (** For brevity, we define the intra-supply interference bound
+      function ([intra_IBF]). Note that in the case of FIFO,
+      intra-supply IBF does not depend on the second argument.  *)
+  Local Definition intra_IBF (A _Δ : duration) :=
+    total_request_bound_function ts (A + ε) - task_cost tsk.
+
+  (** Ultimately, we seek to apply aRSA to prove the correctness of
+      the following [R]. *)
+  Variable R : duration.
+  Hypothesis H_R_is_maximum :
+    forall (A : duration),
+      is_in_search_space ts L A ->
+      exists (F : duration),
+        A <= F <= A + R
+        /\ total_request_bound_function ts (A + ε) <= SBF F.
+
+  (** However, in order to connect the definition of [R] with aRSA, we
+      must first restate the bound in the shape of the abstract
+      response-time bound equation that aRSA expects, which we do
+      next. *)
+
+  (** We know that:
+     - if [A] is in the abstract search space, then it is also in the
+       concrete search space; and
+     - if [A] is in the concrete search space, then there exists a
+       solution that satisfies the inequalities stated in
+       [H_R_is_maximum]. Using these facts, we prove that, if [A] is
+       in the abstract search space, then there also exists a solution
+       [F] to the response-time equation as expected by aRSA. *)
+  Lemma soln_abstract_response_time_recurrence :
+    forall A : duration,
+      abstract.search_space.is_in_search_space L (fifo.IBF ts tsk) A ->
+      exists F : duration,
+        F <= A + R
+        /\ task_rtct tsk + intra_IBF A F <= SBF F
+        /\ SBF F + (task_cost tsk - task_rtct tsk) <= SBF (A + R).
+  Proof.
+    move => A SP; move: (H_R_is_maximum A) => MAX.
+    rewrite /intra_IBF.
+    feed MAX; first by apply: search_space_sub => //.
+    move: MAX => [F' [FE LGL]].
+    have Leq1 : SBF F' <= SBF (A + R) by apply H_SBF_monotone; lia.
+    have Leq2 : total_request_bound_function ts (A + 1) >= task_cost tsk by apply task_cost_le_sum_rbf => //; lia.
+    have Leq3 : task_cost tsk >= task_rtct tsk by apply H_valid_run_to_completion_threshold.
+    unfold total_request_bound_function in *.
+    have [F'' [LE EX]]:
+      exists F'',
+        0 <= F'' <= A + R
+        /\ SBF F'' = SBF (A + R) - (task_cost tsk - task_rtct tsk).
+    { apply exists_intermediate_point_leq.
+      - by move=> t; rewrite !addn1; apply H_unit_SBF.
+      - lia.
+      - apply/andP; split.
+        + rewrite (fst H_valid_SBF); lia.
+        + lia.
+    }
+    exists F''; split; last split.
+    + by move: LE; clear; lia.
+    + by rewrite EX; lia.
+    + by rewrite EX; lia.
+  Qed.
+
+End ConcreteToAbstractFixpointReduction.

analysis/abstract/restricted_supply/search_space/fp.v

+Require Export prosa.analysis.facts.model.rbf.
+Require Export prosa.analysis.abstract.search_space.
+Require Export prosa.analysis.definitions.blocking_bound.fp.
+
+
+(** * Abstract Search Space is a Subset of Restricted Supply FP Search Space *)
+
+(** A response-time analysis usually involves solving the
+    response-time equation for various relative arrival times
+    (w.r.t. the beginning of the corresponding busy interval) of a job
+    under analysis. To reduce the time complexity of the analysis, the
+    state of the art uses the notion of a search space. Intuitively,
+    this corresponds to all "interesting" arrival offsets that the job
+    under analysis might have with regard to the beginning of its busy
+    window.
+
+    In this file, we prove that the search space derived from the aRTA
+    theorem is a subset of the search space for the FP scheduling
+    policy with restricted supply. In other words, by solving the
+    response-time equation for points in the FP search space, one also
+    checks all points in the aRTA search space, which makes FP
+    compatible with aRTA w.r.t. the search space. *)
+Section SearchSpaceSubset.
+
+  (** Consider any type of tasks. *)
+  Context {Task : TaskType}.
+  Context `{TaskCost Task}.
+  Context `{TaskMaxNonpreemptiveSegment Task}.
+
+  (** Consider an FP policy that indicates a higher-or-equal priority
+      relation. *)
+  Context {FP : FP_policy Task}.
+
+  (** Consider an arbitrary task set [ts]. *)
+  Variable ts : list Task.
+
+  (** 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.
+
+  (** Let [tsk] be any task in [ts] that is to be analyzed. *)
+  Variable tsk : Task.
+  Hypothesis H_tsk_in_ts : tsk \in ts.
+
+  (** Let's define some local names for clarity. *)
+  Let task_rbf := task_request_bound_function tsk.
+  Let total_ohep_rbf := total_ohep_request_bound_function_FP ts tsk.
+
+  (** Let [L] be an arbitrary positive constant. Typically, [L]
+      denotes an upper bound on the length of a busy interval of a job
+      of [tsk]. In this file, however, [L] can be any positive
+      constant. *)
+  Variable L : duration.
+  Hypothesis H_L_positive : 0 < L.
+
+  (** For the fixed-priority scheduling policy, the search space is
+      defined as the set of offsets below [L] where the RBF of the
+      task under analysis makes a step. *)
+  Definition is_in_search_space A :=
+    (A < L) && (task_rbf A != task_rbf (A + ε)).
+
+  (** To rule out pathological cases with the search space, we assume
+      that the task cost is positive and the arrival curve is
+      non-pathological. *)
+  Hypothesis H_task_cost_pos : 0 < task_cost tsk.
+  Hypothesis H_arrival_curve_pos : 0 < max_arrivals tsk ε.
+
+  (** For brevity, let us introduce a shorthand for an intra-IBF (used
+      by aRTA). The abstract search space is derived via intra-IBF. *)
+  Let intra_IBF (A F : duration) :=
+    task_rbf (A + ε) - task_cost tsk
+    + (blocking_bound ts tsk + total_ohep_rbf F).
+
+  (** Then, abstract RTA's standard search space is a subset of the
+      computation-oriented version defined above. *)
+  Lemma search_space_sub :
+    forall A,
+      search_space.is_in_search_space L intra_IBF A ->
+      is_in_search_space A.
+  Proof.
+    move => A [ZERO|[/andP [GTA LTA]] [x [LTx NEQ]]]; rewrite /is_in_search_space.
+    { subst; rewrite H_L_positive //=.
+      rewrite /task_rbf task_rbf_0_zero // eq_sym -lt0n add0n.
+      exact: task_rbf_epsilon_gt_0.
+    }
+    { rewrite LTA //=; move: NEQ => /neqP; rewrite neq_ltn => /orP [LT|LT].
+      { rewrite ltn_add2r in LT.
+        have F : forall a b c, a - c < b - c -> a < b by clear; lia.
+        apply F in LT; rewrite subnK in LT => //.
+        by rewrite neq_ltn; apply/orP; left.
+      }
+      { rewrite ltn_add2r in LT.
+        have F : forall a b c, a - c < b - c -> a < b by clear; lia.
+        apply F in LT; rewrite subnK in LT => //.
+        by rewrite neq_ltn; apply/orP; right.
+      }
+    }
+  Qed.
+
+End SearchSpaceSubset.

analysis/abstract/restricted_supply/task_intra_interference_bound.v

+Require Export prosa.analysis.abstract.restricted_supply.abstract_seq_rta.
+Require Export prosa.analysis.abstract.restricted_supply.iw_instantiation.
+Require Export prosa.analysis.definitions.sbf.busy.
+Require Export prosa.analysis.definitions.workload.bounded.
+
+
+(** * Task Intra-Supply Interference is Bounded *)
+
+(** In this file, we define the task intra-supply IBF [task_intra_IBF]
+    assuming that we have two functions: one bounding service
+    inversion and the other bounding the higher-or-equal-priority
+    workload (w.r.t. a job under analysis). We then prove that
+    [task_intra_IBF] indeed bounds the cumulative task intra-supply
+    interference. *)
+Section TaskIntraInterferenceIsBounded.
+
+  (** Consider any type of tasks ... *)
+  Context {Task : TaskType}.
+
+  (**  ... and any type of jobs associated with these tasks. *)
+  Context {Job : JobType}.
+  Context {Cost : JobCost Job}.
+  Context `{JobArrival Job}.
+  Context `{JobTask Job Task}.
+
+  (** Consider any kind of fully supply-consuming unit-supply
+      uniprocessor model. *)
+  Context `{PState : ProcessorState Job}.
+  Hypothesis H_uniprocessor_proc_model : uniprocessor_model PState.
+  Hypothesis H_unit_supply_proc_model : unit_supply_proc_model PState.
+  Hypothesis H_consumed_supply_proc_model : fully_consuming_proc_model PState.
+
+  (** Consider a JLFP policy that indicates a higher-or-equal-priority
+      relation, and assume that the relation is reflexive.
+
+      Note that we do not relate the JLFP policy with the
+      scheduler. However, we define functions for Interference and
+      Interfering Workload that actively use the concept of
+      priorities. We require the JLFP policy to be reflexive, so a job
+      cannot cause lower-priority interference (i.e. priority
+      inversion) to itself. *)
+  Context {JLFP : JLFP_policy Job}.
+  Hypothesis H_priority_is_reflexive : reflexive_job_priorities JLFP.
+
+  (** We also assume that the policy respects sequential tasks,
+      meaning that later-arrived jobs of a task don't have higher
+      priority than earlier-arrived jobs of the same task. *)
+  Hypothesis H_JLFP_respects_sequential_tasks : policy_respects_sequential_tasks JLFP.
+
+  (** Consider any valid arrival sequence ... *)
+  Variable arr_seq : arrival_sequence Job.
+  Hypothesis H_valid_arrival_sequence : valid_arrival_sequence arr_seq.
+
+  (** ... and a schedule of this arrival sequence ... *)
+  Variable sched : schedule PState.
+  Hypothesis H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched arr_seq.
+
+  (** ... where jobs do not execute before their arrival nor after completion. *)
+  Hypothesis H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched.
+  Hypothesis H_completed_jobs_dont_execute : completed_jobs_dont_execute sched.
+
+  (** We say that job [j] incurs interference at time [t] iff it
+      cannot execute due to (1) the lack of supply at time [t], (2)
+      service inversion (i.e., a lower-priority job receiving service
+      at [t]), or a higher-or-equal-priority job receiving service. *)
+  #[local] Instance rs_jlfp_interference : Interference Job :=
+    rs_jlfp_interference arr_seq sched.
+
+  (** The interfering workload, in turn, is defined as the sum of the
+      blackout predicate, service-inversion predicate, and the
+      interfering workload of jobs with higher or equal priority. *)
+  #[local] Instance rs_jlfp_interfering_workload : InterferingWorkload Job :=
+    rs_jlfp_interfering_workload arr_seq sched.
+
+  (** Let [tsk] be any task to be analyzed. *)
+  Variable tsk : Task.
+
+  (** Assume that there exists a bound on the length of any service
+      inversion experienced by any job of task [tsk]. *)
+  Variable service_inversion_bound : duration -> duration.
+  Hypothesis H_service_inversion_is_bounded :
+    service_inversion_is_bounded_by
+     arr_seq sched tsk service_inversion_bound.
+
+  (** Assume that there exists a bound on the higher-or-equal-priority
+      (w.r.t. a [tsk]'s job) workload of tasks different from [tsk]. *)
+  Variable athep_workload_bound : (* A *) duration -> (* Δ *) duration -> duration.
+  Hypothesis H_workload_is_bounded :
+    athep_workload_is_bounded arr_seq sched tsk athep_workload_bound.
+
+  (** Finally, we define the interference-bound function ([task_intra_IBF]). *)
+  Definition task_intra_IBF (A R : duration) :=
+    service_inversion_bound A + athep_workload_bound A R.
+
+  (** Next, we prove that [task_intra_IBF] is indeed an interference bound. *)
+  Lemma instantiated_task_intra_interference_is_bounded :
+    task_intra_interference_is_bounded_by
+      arr_seq sched tsk task_intra_IBF.
+  Proof.
+    move => t1 t2 Δ j ARR TSK BUSY LT NCOMPL A OFF.
+    move: (OFF _ _ BUSY) => EQA; subst A.
+    have [ZERO|POS] := posnP (@job_cost _ Cost j).
+    { by exfalso; rewrite /completed_by ZERO in NCOMPL. }
+    eapply leq_trans; first by eapply cumulative_task_interference_split => //.
+    rewrite /task_intra_IBF leq_add//.
+    { apply leq_trans with (cumulative_service_inversion arr_seq sched j t1 (t1 + Δ)); first by done.
+      apply leq_trans with (cumulative_service_inversion arr_seq sched j t1 t2); last first.
+      { apply: H_service_inversion_is_bounded; eauto 2 => //.
+        apply abstract_busy_interval_classic_busy_interval_prefix => //. }
+      by rewrite [X in _ <= X](@big_cat_nat _ _ _ (t1 + Δ)) //= leq_addr. }
+    { erewrite cumulative_i_thep_eq_service_of_othep; eauto 2 => //; last first.
+      { by apply instantiated_quiet_time_equivalent_quiet_time => //; apply BUSY. }
+      apply: leq_trans.
+      { by apply service_of_jobs_le_workload => //; apply unit_supply_is_unit_service. }
+      { by apply H_workload_is_bounded => //; apply: abstract_busy_interval_classic_quiet_time => //. }
+    }
+  Qed.
+
+End TaskIntraInterferenceIsBounded.

restructuring/analysis/abstract/core/reduction_of_search_space.v → analysis/abstract/search_space.v

-Require Import rt.util.epsilon.
-Require Import rt.util.tactics.
-Require Import rt.restructuring.model.task.concept.
-From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
+Require Import prosa.util.epsilon.
+Require Import prosa.util.tactics.
+Require Import prosa.model.task.concept.
 
-(** * Reduction of the serach space for Abstract RTA *)
+(** * Reduction of the search space for Abstract RTA *)
 (** In this file, we prove that in order to calculate the worst-case response time 
-    it is sufficient to consider only values of A that lie in the search space defined below. *)  
+    it is sufficient to consider only values of [A] that lie in the search space defined below. *)  
 
 Section AbstractRTAReduction. 
 
   (** The response-time analysis we are presenting in this series of documents is based on searching 
-     over all possible values of A, the relative arrival time of the job respective to the beginning 
+     over all possible values of [A], the relative arrival time of the job respective to the beginning 
      of the busy interval. However, to obtain a practically useful response-time bound, we need to 
-     constrain the search space of values of A. In this section, we define an approach to 
+     constrain the search space of values of [A]. In this section, we define an approach to 
      reduce the search space. *)
   
   Context {Task : TaskType}.
@@ -20,78 +19,78 @@ Section AbstractRTAReduction.
   (** First, we provide a constructive notion of equivalent functions. *)
   Section EquivalentFunctions.
     
-    (** Consider an arbitrary type T... *)
+    (** Consider an arbitrary type [T]... *)
     Context {T : eqType}.
 
-    (**  ...and two function from nat to T. *)
+    (**  ...and two function from [nat] to [T]. *)
     Variables f1 f2 : nat -> T.
 
-    (** Let B be an arbitrary constant. *) 
+    (** Let [B] be an arbitrary constant. *) 
     Variable B : nat.
     
-    (** Then we say that f1 and f2 are equivalent at values less than B iff
-       for any natural number x less than B [f1 x] is equal to [f2 x].  *)
+    (** Then we say that [f1] and [f2] are equivalent at values less than [B] iff
+       for any natural number [x] less than [B] [f1 x] is equal to [f2 x].  *)
     Definition are_equivalent_at_values_less_than :=
       forall x, x < B -> f1 x = f2 x.
 
-    (** And vice versa, we say that f1 and f2 are not equivalent at values 
-       less than B iff there exists a natural number x less than B such
+    (** And vice versa, we say that [f1] and [f2] are not equivalent at values 
+       less than [B] iff there exists a natural number [x] less than [B] such
        that [f1 x] is not equal to [f2 x].  *)
     Definition are_not_equivalent_at_values_less_than :=
       exists x, x < B /\ f1 x <> f2 x.
 
   End EquivalentFunctions. 
 
-  (** Let tsk be any task that is to be analyzed *)
+  (** Let [tsk] be any task that is to be analyzed *)
   Variable tsk : Task.
   
-  (** To ensure that the analysis procedure terminates, we assume an upper bound B on 
-     the values of A that must be checked. The existence of B follows from the assumption 
+  (** To ensure that the analysis procedure terminates, we assume an upper bound [B] on 
+     the values of [A] that must be checked. The existence of [B] follows from the assumption 
      that the system is not overloaded (i.e., it has bounded utilization). *)
   Variable B : duration.
 
   (** Instead of searching for the maximum interference of each individual job, we 
-     assume a per-task interference bound function [IBF(tsk, A, x)] that is parameterized 
-     by the relative arrival time A of a potential job (see abstract_RTA.definitions.v file). *)
-  Variable interference_bound_function : Task -> duration -> duration -> duration.
-
-  (** Recall the definition of ε, which defines the neighborhood of a point in the timeline.
-     Note that epsilon = 1 under discrete time. *)
-  (** To ensure that the search converges more quickly, we only check values of A in the interval 
-     [0, B) for which the interference bound function changes, i.e., every point x in which 
-     interference_bound_function (A - ε, x) is not equal to interference_bound_function (A, x). *)
+     assume a per-task interference bound function [IBF(A, x)] that is parameterized 
+     by the relative arrival time [A] of a potential job (see abstract_RTA.definitions.v file). *)
+  Variable interference_bound_function : duration -> duration -> duration.
+
+  (** Recall the definition of [ε], which defines the neighborhood of a point in the timeline.
+     Note that [ε = 1] under discrete time. *)
+  (** To ensure that the search converges more quickly, we only check values of [A] in the interval 
+     <<[0, B)>> for which the interference bound function changes, i.e., every point [x] in which 
+     [interference_bound_function (A - ε, x)] is not equal to [interference_bound_function (A, x)]. *)
   Definition is_in_search_space A :=
     A = 0 \/
     0 < A < B /\ are_not_equivalent_at_values_less_than
-                  (interference_bound_function tsk (A - ε)) (interference_bound_function tsk A) B.
+                  (interference_bound_function (A - ε)) (interference_bound_function A) B.
   
-  (** In this section we prove that for every A there exists a smaller A_sp 
-     in the search space such that interference_bound_function(A_sp,x) is 
-     equal to interference_bound_function(A, x). *)
+  (** In this section we prove that for every [A] there exists a smaller [A_sp] 
+     in the search space such that [interference_bound_function(A_sp,x)] is 
+     equal to [interference_bound_function(A, x)]. *)
   Section ExistenceOfRepresentative.
 
-    (** Let A be any constant less than B. *) 
+    (** Let [A] be any constant less than [B]. *) 
     Variable A : duration.
     Hypothesis H_A_less_than_B : A < B.
     
-    (** We prove that there exists a constant A_sp such that:
-       (a) A_sp is no greater than A, (b) interference_bound_function(A_sp, x) is 
-       equal to interference_bound_function(A, x) and (c) A_sp is in the search space.
-       In other words, either A is already inside the search space, or we can go 
-       to the "left" until we reach A_sp, which will be inside the search space. *)
+    (** We prove that there exists a constant [A_sp] such that:
+       (a) [A_sp] is no greater than [A], (b) [interference_bound_function(A_sp, x)] is 
+       equal to [interference_bound_function(A, x)] and (c) [A_sp] is in the search space.
+       In other words, either [A] is already inside the search space, or we can go 
+       to the "left" until we reach [A_sp], which will be inside the search space. *)
     Lemma representative_exists:
       exists A_sp, 
         A_sp <= A /\
-        are_equivalent_at_values_less_than (interference_bound_function tsk A)
-                                           (interference_bound_function tsk A_sp) B /\
+        are_equivalent_at_values_less_than (interference_bound_function A)
+                                           (interference_bound_function A_sp) B /\
         is_in_search_space A_sp.
     Proof.
-      induction A as [|n].
+      induction A as [|n IHn].
       - exists 0; repeat split.
           by rewrite /is_in_search_space; left.
       - have ALT:
-          all (fun t => interference_bound_function tsk n t == interference_bound_function tsk n.+1 t) (iota 0 B)
-          \/ has (fun t => interference_bound_function tsk n t != interference_bound_function tsk n.+1 t) (iota 0 B).
+          all (fun t => interference_bound_function n t == interference_bound_function n.+1 t) (iota 0 B)
+          \/ has (fun t => interference_bound_function n t != interference_bound_function n.+1 t) (iota 0 B).
         { apply/orP.
           rewrite -[_ || _]Bool.negb_involutive Bool.negb_orb.
           apply/negP; intros CONTR.
@@ -101,56 +100,54 @@ Section AbstractRTAReduction.
         feed IHn; first by apply ltn_trans with n.+1. 
         move: IHn => [ASP [NEQ [EQ SP]]].
         move: ALT => [/allP ALT| /hasP ALT].
-        { exists ASP; repeat split; try done.
-          { by apply leq_trans with n. }
-          { intros x LT.
-            move: (ALT x) => T. feed T; first by rewrite mem_iota; apply/andP; split. 
-            move: T => /eqP T.
-              by rewrite -T EQ.
-          }
+        { exists ASP; repeat split=> //.
+          intros x LT.
+          move: (ALT x) => T.
+          feed T; first by rewrite mem_iota; apply/andP; split.
+          by move: T => /eqP<-; rewrite EQ.
         }
-        { exists n.+1; repeat split; try done.
+        { exists n.+1; repeat split=> //.
           rewrite /is_in_search_space; right.
           split; first by  apply/andP; split.
           move: ALT => [y IN N].
           exists y.
           move: IN; rewrite mem_iota add0n. move => /andP [_ LT]. 
-          split; first by done.
+          split=> [//|].
           rewrite subn1 -pred_Sn.
           intros CONTR; move: N => /negP N; apply: N.
-            by rewrite CONTR.
+          by rewrite CONTR.
         }
     Qed.
 
   End ExistenceOfRepresentative.
 
   (** In this section we prove that any solution of the response-time recurrence for
-     a given point A_sp in the search space also gives a solution for any point 
+     a given point [A_sp] in the search space also gives a solution for any point 
      A that shares the same interference bound. *)
   Section FixpointSolutionForAnotherA.
 
-    (** Suppose A_sp + F_sp is a "small" solution (i.e. less than B) of the response-time recurrence. *)
+    (** Suppose [A_sp + F_sp] is a "small" solution (i.e. less than [B]) of the response-time recurrence. *)
     Variables A_sp F_sp : duration.
     Hypothesis H_less_than : A_sp + F_sp < B.
-    Hypothesis H_fixpoint : A_sp + F_sp = interference_bound_function tsk A_sp (A_sp + F_sp).
+    Hypothesis H_fixpoint : A_sp + F_sp >= interference_bound_function A_sp (A_sp + F_sp).
 
-    (** Next, let A be any point such that: (a) A_sp <= A <= A_sp + F_sp and 
-       (b) interference_bound_function(A, x) is equal to 
-       interference_bound_function(A_sp, x) for all x less than B. *)
+    (** Next, let [A] be any point such that: (a) [A_sp <= A <= A_sp + F_sp] and 
+       (b) [interference_bound_function(A, x)] is equal to 
+       [interference_bound_function(A_sp, x)] for all [x] less than [B]. *)
     Variable A : duration.
     Hypothesis H_bounds_for_A : A_sp <= A <= A_sp + F_sp.
     Hypothesis H_equivalent :
       are_equivalent_at_values_less_than
-        (interference_bound_function tsk A)
-        (interference_bound_function tsk A_sp) B.
+        (interference_bound_function A)
+        (interference_bound_function A_sp) B.
 
-    (** We prove that there exists a consant F such that [A + F] is equal to [A_sp + F_sp]
-       and [A + F] is a solution for the response-time recurrence for A. *)
+    (** We prove that there exists a constant [F] such that [A + F] is equal to [A_sp + F_sp]
+       and [A + F] is a solution for the response-time recurrence for [A]. *)
     Lemma solution_for_A_exists:
       exists F,
         A_sp + F_sp = A + F /\
         F <= F_sp /\
-        A + F = interference_bound_function tsk A (A + F).
+        A + F >= interference_bound_function A (A + F).
     Proof.  
       move: H_bounds_for_A => /andP [NEQ1 NEQ2].
       set (X := A_sp + F_sp) in *.
@@ -161,6 +158,40 @@ Section AbstractRTAReduction.
     Qed.
 
   End FixpointSolutionForAnotherA.
-  
+
 End AbstractRTAReduction.
 
+(** In this section, we prove a simple lemma that allows one to switch
+    IBFs inside of the [is_in_search_space] predicate. *)
+Section SearchSpaceSwitch.
+
+  (** Consider any type of tasks. *)
+  Context {Task : TaskType}.
+
+  (** Let [tsk] be any task that is to be analyzed. *)
+  Variable tsk : Task.
+
+  (** Similarly to the previous section, to ensure that the analysis
+      procedure terminates, we assume an upper bound [B] on the values
+      of [A] that must be checked. *)
+  Variable B : duration.
+
+  (** Given two IBFs [IBF1] and [IBF2] such that they are equal for
+      all inputs, if an offset [A] is in the search space of [IBF1],
+      then [A] is in the search space of [IBF2]. *)
+  Lemma search_space_switch_IBF :
+    forall IBF1 IBF2,
+      (forall A Δ, A < B -> IBF1 A Δ = IBF2 A Δ) ->
+      forall A,
+        is_in_search_space B IBF1 A ->
+        is_in_search_space B IBF2 A.
+  Proof.
+    move=> IBF1 IBF2 EQU A [EQ|[NEQ NEQU]]; first by left; subst.
+    right; split; first by done.
+    move: NEQU => [x [LT NEQf]].
+    exists x; split; first by done.
+    move: NEQf.
+    by rewrite !EQU //=; lia.
+  Qed.
+
+End SearchSpaceSwitch.

analysis/definitions/always_higher_priority.v

+Require Export prosa.model.priority.classes.
+
+(** * Always Higher Priority *)
+(** In this section, we define what it means for a job to always have
+    a higher priority than another job. *)
+Section AlwaysHigherPriority.
+
+  (** Consider any type of jobs ... *)
+  Context {Job : JobType}.
+
+  (** ... and any JLDP policy. *)
+  Context `{JLDP_policy Job}.
+
+  (** We say that a job [j1] always has higher priority than job [j2]
+      if, at any time [t], the priority of job [j1] is strictly higher than
+      the priority of job [j2]. *)
+  Definition always_higher_priority (j1 j2 : Job) :=
+    forall t, hep_job_at t j1 j2 && ~~ hep_job_at t j2 j1.
+
+End AlwaysHigherPriority.
+
+(** We note that, under a job-level fixed-priority policy, the property is
+    trivial since job priorities by definition do not change in this case. *)
+Section UnderJLFP.
+  (** Consider any type of jobs ... *)
+  Context {Job : JobType}.
+
+  (** ... and any JLFP policy. *)
+  Context `{JLFP_policy Job}.
+
+  (** The property [always_higher_priority j j'] is equivalent to a statement
+      about [hep_job]. *)
+  Fact always_higher_priority_jlfp :
+    forall j j',
+      always_higher_priority j j' <-> (hep_job j j' && ~~ hep_job j' j).
+  Proof.
+    by move=> j j'; split => [|HP t]; [apply; exact: 0 | rewrite !hep_job_at_jlfp].
+  Qed.
+
+End UnderJLFP.