Require Import prosa.classic.util.all.
Require Import prosa.classic.model.arrival.basic.job.
Require Import prosa.classic.model.schedule.uni.service
               prosa.classic.model.schedule.uni.schedule
               prosa.classic.model.schedule.uni.response_time.
Require Import prosa.classic.model.schedule.uni.limited.schedule
               prosa.classic.model.schedule.uni.limited.abstract_RTA.definitions
               prosa.classic.model.schedule.uni.limited.abstract_RTA.sufficient_condition_for_lock_in_service
               prosa.classic.model.schedule.uni.limited.abstract_RTA.reduction_of_search_space.

From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.

Module AbstractRTA.

  Import Job UniprocessorSchedule Service ResponseTime AbstractRTADefinitions
         AbstractRTALockInService AbstractRTAReduction.

  (* In this section we prove that the maximum among the solutions of the response-time bound 
     recurrence is a response time bound for tsk. Note that in this section we do not rely on 
     any hypotheses about job sequentiality. *)
  Section Abstract_RTA.

    Context {Task: eqType}.
    Variable task_cost: Task → time.

    Context {Job: eqType}.
    Variable job_arrival: Job → time.
    Variable job_cost: Job → time.
    Variable job_task: Job → Task.

    (* Consider any arrival sequence with consistent, non-duplicate arrivals... *)
    Variable arr_seq: arrival_sequence Job.
    Hypothesis H_arrival_times_are_consistent: arrival_times_are_consistent job_arrival arr_seq.
    Hypothesis H_arr_seq_is_a_set: arrival_sequence_is_a_set arr_seq.

    (* Next, consider any uniprocessor schedule of this arrival sequence...*)
    Variable sched: schedule Job.
    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 job_arrival sched.
    Hypothesis H_completed_jobs_dont_execute: completed_jobs_dont_execute job_cost sched.

    (* Assume that the job costs are no larger than the task costs. *)
    Hypothesis H_job_cost_le_task_cost:
      cost_of_jobs_from_arrival_sequence_le_task_cost
        task_cost job_cost job_task 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 proper job lock-in service and task lock-in service functions, i.e... *)
    Variable job_lock_in_service: Job → time.
    Variable task_lock_in_service: Task → time.

    (* ...we assume that for all jobs in the arrival sequence the lock-in service is 
       (1) positive, (2) no bigger than the costs of the corresponding jobs, and 
       (3) a job becomes nonpreemptive after it reaches its lock-in service... *)
    Hypothesis H_proper_job_lock_in_service:
      proper_job_lock_in_service job_cost arr_seq sched job_lock_in_service.

    (* ...and that task_lock_in_service tsk is (1) no bigger than tsk's cost, (2) for any
       job of task tsk job_lock_in_service is bounded by task_lock_in_service. *)
    Hypothesis H_proper_task_lock_in_service:
      proper_task_lock_in_service
        task_cost job_task arr_seq job_lock_in_service task_lock_in_service tsk.

     (* Let's define some local names for clarity. *)
    Let work_conserving := work_conserving job_arrival job_cost job_task arr_seq sched tsk.
    Let busy_intervals_are_bounded_by := busy_intervals_are_bounded_by job_arrival job_cost job_task arr_seq sched tsk.
    Let job_interference_is_bounded_by := job_interference_is_bounded_by job_arrival job_cost job_task arr_seq sched tsk.

    (* Assume we are provided with abstract functions for interference and interfering workload. *)
    Variable interference: Job → time → bool.
    Variable interfering_workload: Job → time → time.

    (* We assume that the scheduler is work-conserving. *)
    Hypothesis H_work_conserving: work_conserving interference interfering_workload.

    (* For simplicity, let's define some local names. *)
    Let cumul_interference := cumul_interference interference.
    Let cumul_interfering_workload := cumul_interfering_workload interfering_workload.
    Let busy_interval := busy_interval job_arrival job_cost sched interference interfering_workload.
    Let response_time_bounded_by :=
      is_response_time_bound_of_task job_arrival job_cost job_task arr_seq sched.

    (* Let L be a constant which bounds any busy interval of task tsk. *)
    Variable L: time.
    Hypothesis H_busy_interval_exists: busy_intervals_are_bounded_by interference interfering_workload L.

    (* Next, assume that interference_bound_function is a bound on 
       the interference incurred by jobs of task tsk. *)
    Variable interference_bound_function: Task → time → time → time.
    Hypothesis H_job_interference_is_bounded:
      job_interference_is_bounded_by interference interfering_workload interference_bound_function.

    (* For simplicity, let's define a local name for the search space. *)
    Let is_in_search_space A := is_in_search_space tsk L interference_bound_function A.

    (* 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 F + (task_cost tsk - task_lock_in_service tsk) <= R. *)
    Variable R: nat.
    Hypothesis H_R_is_maximum:
      ∀ A,
        is_in_search_space A →
        ∃ F,
          A + F = task_lock_in_service tsk + interference_bound_function tsk A (A + F) ∧
          F + (task_cost tsk - task_lock_in_service tsk) ≤ R.

    (* In this section we show a detailed proof of the main theorem 
       that establishes that R is a response-time bound of task tsk. *)
    Section ProofOfTheorem.

      (* Consider any job j of tsk. *)
      Variable j: Job.
      Hypothesis H_j_arrives: arrives_in arr_seq j.
      Hypothesis H_job_of_tsk: job_task j = tsk.
      Hypothesis H_job_cost_positive: job_cost_positive job_cost j.

      (* Assume we have a busy interval t1, t2) of job j that is bounded by L. *)
      Variable t1 t2: time.
      Hypothesis H_busy_interval: busy_interval j t1 t2.

      (* Let's define A as a relative arrival time of job j (with respect to time t1). *)
      Let A := job_arrival j - t1.

      (* In order to prove that R is a response-time bound of job j, we use hypothesis H_R_is_maximum. 
         Note that the relative arrival time (A) is not necessarily from the search space. However, 
         earlier we have proven that for any A there exists another A_sp from the search space that
         shares the same IBF value. Moreover, we've also shown that there exists an F_sp such that
         F_sp is a solution of the response time recurrence for parameter A_sp. Thus, despite the 
         fact that the relative arrival time may not lie in the search space, we can still use
         the assumption H_R_is_maximum. *)

      (* More formally, consider any A_sp and F_sp such that:.. *)
      Variable A_sp F_sp: time.
      (* (a) A_sp is less than or equal to A... *)
      Hypothesis H_A_gt_Asp: A_sp ≤ A.
      (* (b) interference_bound_function(A, x) is equal to interference_bound_function(A_sp, x) for all x less than L... *)
      Hypothesis H_equivalent:
        are_equivalent_at_values_less_than (interference_bound_function tsk A) (interference_bound_function tsk A_sp) L.
      (* (c) A_sp is in the search space, ... *)
      Hypothesis H_Asp_is_in_search_space: is_in_search_space A_sp.
      (* (d) A_sp + F_sp is a solution of the response time reccurence... *)
      Hypothesis H_fixpoint:
        A_sp + F_sp = task_lock_in_service tsk + interference_bound_function tsk A_sp (A_sp + F_sp).
      (* (e) and finally, F_sp + (task_last - ε) is no greater than R. *)
      Hypothesis H_R_gt_Fsp: F_sp + (task_cost tsk - task_lock_in_service tsk) ≤ R.

      (* In this section, we consider the case where the solution is so large that the value of t1 + A_sp + F_sp goes 
         beyond the busy interval. Although this case may be impossible in some scenarios, it can be easily proven,
         since any job that completes by the end of the busy interval remains completed. *)
      Section FixpointOutsideBusyInterval.

        (* By assumption, suppose that t2 is less than or equal to t1 + A_sp + F_sp. *)
        Hypothesis H_big_fixpoint_solution: t2 ≤ t1 + (A_sp + F_sp).

        (* Then we prove that (job_arrival j + R) is no less than t2. *)
        Lemma t2_le_arrival_plus_R:
          t2 ≤ job_arrival j + R.

        (* But since we know that the job is completed by the end of its busy interval, 
           we can show that job j is completed by (job arrival j + R) *)
        Lemma job_completed_by_arrival_plus_R_1:
          completed_by job_cost sched j (job_arrival j + R).

      End FixpointOutsideBusyInterval.

      (* In this section, we consider the complementary case where t1 + A_sp + F_sp lies inside the busy interval. *)
      Section FixpointInsideBusyInterval.

        (* So, assume that t1 + A_sp + F_sp is less than t2. *)
        Hypothesis H_small_fixpoint_solution: t1 + (A_sp + F_sp) < t2.

        (* Next, let's consider two other cases: *)
        (* CASE 1: the value of the fixpoint is no less than the relative arrival time of job j. *)
        Section FixpointIsNoLessThanArrival.

          (* Suppose that A_sp + F_sp is no less than relative arrival of job j. *)
          Hypothesis H_fixpoint_is_no_less_than_relative_arrival_of_j: A ≤ A_sp + F_sp.

          (* Using lemma "solution_for_A_exists" we can find a solution for response time recurrence for A. *)
          Lemma solution_for_A_exists':
            ∃ F,
              A_sp + F_sp = A + F ∧
              F ≤ F_sp ∧
              A + F = task_lock_in_service tsk + interference_bound_function tsk A (A + F).

          (* To prove this lemma, we introduce two temporal notions of the last nonpreemptive region of job j 
             and an execution optimism. We use these notions only inside this proof, so we don't define them
             explicitly. Let the last nonpreemptive region of job j (last) be the difference between the cost 
             of the job and the j's lock-in service (i.e. job_cost j - job_lock_in_service j). We know that
             after j has reached its lock-in service, it will additionally be executed last units of time. 
             And let execution optimism (optimism) be the difference between the tsk's lock-in service 
             and the j's lock-in service (i.e. task_lock_in_service - job_lock_in_service). And optimism is 
             how much earlier job j has received its lock-in service than it could at worst. From lemma 
             j_receives_at_least_lock_in_service we know that service of j by time t1 + (A + F) - optimism 
             is no less than lock_in_service j. Hence, job j is completed by time t1 + (A + F) - optimism + last 
             which is smaller than job_arrival j + R. *)
          Lemma job_completed_by_arrival_plus_R_2:
            completed_by job_cost sched j (job_arrival j + R).

        End FixpointIsNoLessThanArrival.

        (* CASE 2: the value of the fixpoint is less than the relative arrival time of 
           job j (which turns out to be impossible, i.e. the solution of the responce-time 
           recurrense is always equal to or greater than the relative arrival time). *)
        Section FixpointCannotBeSmallerThanArrival.

          (* Assume that A_sp + F_sp is less than A. *)
          Hypothesis H_fixpoint_is_less_that_relative_arrival_of_j: A_sp + F_sp < A.

          (* Note that the relative arrival time of job j is less than L. *)
          Lemma relative_arrival_is_bounded: A < L.

          (* We can use j_receives_at_least_lock_in_service to prove that the service 
             received by j by time t1 + (A_sp + F_sp) is no less than lock_in_service. *)
          Lemma service_of_job_ge_lock_in_service:
            service sched j (t1 + (A_sp + F_sp)) ≥ job_lock_in_service j.

          (* However, this is a contradiction. Since job j has not yet arrived, its 
             service it equal to 0. However, lock_in_service is always positive. *)
          Lemma relative_arrival_time_is_no_less_than_fixpoint:
            False.

        End FixpointCannotBeSmallerThanArrival.

      End FixpointInsideBusyInterval.

    End ProofOfTheorem.

    (* Using the lemmas above, we prove that R is a response-time bound. *)
    Theorem uniprocessor_response_time_bound:
      response_time_bounded_by tsk R.

  End Abstract_RTA.

End AbstractRTA.