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.
Require Import prosa.classic.model.schedule.uni.limited.schedule
               prosa.classic.model.schedule.uni.limited.abstract_RTA.definitions.

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

Module AbstractRTALockInService.

  Import Job UniprocessorSchedule Service AbstractRTADefinitions.

  Section LockInService.

    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.

    Variable arr_seq: arrival_sequence Job.
    Hypothesis H_arrival_times_are_consistent: arrival_times_are_consistent job_arrival arr_seq.

    Variable sched: schedule Job.

    Hypothesis H_job_cost_le_task_cost:
      cost_of_jobs_from_arrival_sequence_le_task_cost
        task_cost job_cost job_task arr_seq.

    Variable tsk: Task.

    Variable interference: Job → time → bool.
    Variable interfering_workload: Job → time → time.

    Let work_conserving := work_conserving job_arrival job_cost job_task arr_seq sched tsk.
    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.

    Hypothesis H_work_conserving: work_conserving interference interfering_workload.

    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.

    Variable t1 t2: time.
    Hypothesis H_busy_interval: busy_interval j t1 t2.

    Lemma job_completes_within_busy_interval:
      completed_by job_cost sched j t2.

    Section InterferenceIsComplement.

      Variable t delta: time.
      Hypothesis H_greater_than_or_equal: t1 ≤ t.
      Hypothesis H_less_or_equal: t + delta ≤ t2.

      Lemma interference_is_complement_to_schedule:
        service_during sched j t (t + delta) + cumul_interference j t (t + delta) = delta.

    End InterferenceIsComplement.

    Section InterferenceBoundedImpliesEnoughService.

      Variable progress_of_job: time.
      Hypothesis H_progress_le_job_cost: progress_of_job ≤ job_cost j.

      Variable delta: time.
      Hypothesis H_total_workload_is_bounded:
        progress_of_job + cumul_interference j t1 (t1 + delta) ≤ delta.

      Theorem j_receives_at_least_lock_in_service:
        service sched j (t1 + delta) ≥ progress_of_job.

    End InterferenceBoundedImpliesEnoughService.

    Section CompletionOfJobAfterLockInService.

      Hypothesis H_completed_jobs_dont_execute:
        completed_jobs_dont_execute job_cost sched.

      Variable job_lock_in_service: Job → time.

      Hypothesis H_lock_in_service_positive:
        job_lock_in_service_positive job_cost arr_seq job_lock_in_service.

      Hypothesis H_lock_in_service_le_job_cost:
        job_lock_in_service_le_job_cost job_cost arr_seq job_lock_in_service.

      Hypothesis H_job_nonpreemptive_after_lock_in_service:
        job_nonpreemptive_after_lock_in_service job_cost arr_seq sched job_lock_in_service.

      Lemma job_completes_after_reaching_lock_in_service:
        ∀ t,
          job_lock_in_service j ≤ service sched j t →
          completed_by job_cost sched j (t + (job_cost j - job_lock_in_service j)).

    End CompletionOfJobAfterLockInService.

  End LockInService.

End AbstractRTALockInService.