Library prosa.classic.analysis.uni.susp.sustainability.allcosts.reduction_properties

Require Import prosa.classic.util.all.
Require Import prosa.classic.model.priority prosa.classic.model.suspension.
Require Import prosa.classic.model.arrival.basic.arrival_sequence.
Require Import prosa.classic.model.schedule.uni.response_time.
Require Import prosa.classic.model.schedule.uni.susp.suspension_intervals
               prosa.classic.model.schedule.uni.susp.schedule
               prosa.classic.model.schedule.uni.susp.valid_schedule
               prosa.classic.model.schedule.uni.susp.build_suspension_table
               prosa.classic.model.schedule.uni.susp.platform.
Require Import prosa.classic.analysis.uni.susp.sustainability.allcosts.reduction.
Require Import prosa.classic.model.schedule.uni.transformation.construction.

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

Module SustainabilityAllCostsProperties.

  Import ScheduleWithSuspensions Suspension Priority SuspensionIntervals
         PlatformWithSuspensions ResponseTime ScheduleConstruction
         SuspensionTableConstruction ValidSuspensionAwareSchedule.

  Module reduction := SustainabilityAllCosts.

  Section ReductionProperties.

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

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

    Variable higher_eq_priority: JLDP_policy Job.
    Hypothesis H_priority_is_reflexive: JLDP_is_reflexive higher_eq_priority.
    Hypothesis H_priority_is_transitive: JLDP_is_transitive higher_eq_priority.
    Hypothesis H_priority_is_total: JLDP_is_total arr_seq higher_eq_priority.

    Variable sched_susp: schedule Job.
    Hypothesis H_jobs_come_from_arrival_sequence:
      jobs_come_from_arrival_sequence sched_susp arr_seq.

    Variable job_suspension_duration: job_suspension Job.

    Hypothesis H_jobs_must_arrive_to_execute:
      jobs_must_arrive_to_execute job_arrival sched_susp.

    Hypothesis H_completed_jobs_dont_execute:
      completed_jobs_dont_execute job_cost sched_susp.

    Hypothesis H_work_conserving:
      work_conserving job_arrival job_cost job_suspension_duration arr_seq sched_susp.

    Hypothesis H_respects_priority:
      respects_JLDP_policy job_arrival job_cost job_suspension_duration arr_seq
                           sched_susp higher_eq_priority.

    Hypothesis H_respects_self_suspensions:
      respects_self_suspensions job_arrival job_cost job_suspension_duration sched_susp.

    Variable j: Job.
    Let arr_j := job_arrival j.

    Variable R: time.

    Variable inflated_job_cost: Job → time.

    Hypothesis H_job_costs_do_not_decrease:
      ∀ any_j, inflated_job_cost any_j ≥ job_cost any_j.

    Let sched_new := reduction.sched_new job_arrival job_cost arr_seq higher_eq_priority
                                         sched_susp inflated_job_cost j R.

    Let suspended_in_sched_new :=
      reduction.suspended_in_sched_new job_arrival job_cost arr_seq higher_eq_priority
                                 sched_susp job_suspension_duration inflated_job_cost j R.

    Let reduced_suspension_duration :=
      reduction.reduced_suspension_duration job_arrival job_cost arr_seq higher_eq_priority
                                   sched_susp job_suspension_duration inflated_job_cost j R.

    Let job_response_time_in_sched_susp_bounded_by :=
      is_response_time_bound_of_job job_arrival job_cost sched_susp.
    Let job_response_time_in_sched_new_bounded_by :=
      is_response_time_bound_of_job job_arrival inflated_job_cost sched_new.
    Let suspended_in_sched_susp :=
      suspended_at job_arrival job_cost job_suspension_duration sched_susp.
    Let job_is_late := reduction.job_is_late job_cost sched_susp inflated_job_cost sched_new.
    Let build_schedule := reduction.build_schedule job_arrival job_cost arr_seq higher_eq_priority
                                                   sched_susp inflated_job_cost j R.
    Let late_or_sched_jobs := reduction.jobs_that_are_late_or_scheduled_in_sched_susp
                                job_arrival job_cost arr_seq sched_susp inflated_job_cost sched_new.
    Let hp_job := reduction.highest_priority_job job_arrival arr_seq higher_eq_priority
                                                 inflated_job_cost sched_new.
    Let hp_late_job := reduction.highest_priority_late_job job_arrival job_cost arr_seq
                                       higher_eq_priority sched_susp inflated_job_cost sched_new.
    Let completed_in_sched_susp := completed_by job_cost sched_susp.
    Let completed_in_sched_new := completed_by inflated_job_cost sched_new.

    Section PropertiesOfScheduleConstruction.

      Lemma sched_new_depends_only_on_service:
        ∀ sched1 sched2 t,
          (∀ j, service sched1 j t = service sched2 j t) →
          build_schedule sched1 t = build_schedule sched2 t.

      Corollary sched_new_uses_construction_function:
        ∀ t,
          sched_new t = build_schedule sched_new t.

    End PropertiesOfScheduleConstruction.

    Section BasicScheduleProperties.

      Lemma sched_new_jobs_come_from_arrival_sequence:
        jobs_come_from_arrival_sequence sched_new arr_seq.

      Lemma sched_new_jobs_must_arrive_to_execute:
        jobs_must_arrive_to_execute job_arrival sched_new.

      Lemma sched_new_completed_jobs_dont_execute:
        completed_jobs_dont_execute inflated_job_cost sched_new.

    End BasicScheduleProperties.

    Section ServiceInvariant.

      Variable t: time.
      Hypothesis H_before_R: t ≤ arr_j + R.

      Lemma sched_new_service_invariant:
        ∀ any_j,
          service sched_new any_j t
            ≤ service sched_susp any_j t + (inflated_job_cost any_j - job_cost any_j).

      Corollary sched_new_jobs_complete_later:
        ∀ any_j,
          completed_by inflated_job_cost sched_new any_j t →
          completed_by job_cost sched_susp any_j t.

    End ServiceInvariant.

    Section SuspensionPredicate.

      Variable any_j: Job.

      Lemma suspended_in_sched_new_implies_arrived:
        ∀ t,
          suspended_in_sched_new any_j t → has_arrived job_arrival any_j t.

      Lemma suspended_in_sched_new_implies_not_completed:
        ∀ t,
          suspended_in_sched_new any_j t → ~~ completed_in_sched_new any_j t.

      Lemma executes_before_suspension_in_sched_new:
        ∀ t,
          t < arr_j + R →
          has_arrived job_arrival any_j t →
          ~~ suspended_in_sched_new any_j t →
          suspended_in_sched_new any_j t.+1 →
          scheduled_at sched_new any_j t.

      Let suspension_start := time_after_last_execution job_arrival.

      Lemma suspended_in_sched_new_no_service_since_execution:
        ∀ t t_mid,
          suspended_in_sched_new any_j t →
          suspension_start sched_new any_j t ≤ t_mid < t →
          service sched_new any_j t ≤ service sched_new any_j t_mid.

      Lemma suspended_in_sched_new_suspension_starts_no_earlier:
        ∀ t,
          has_arrived job_arrival any_j t →
          suspended_in_sched_new any_j t →
          suspension_start sched_susp any_j t ≤ suspension_start sched_new any_j t.

      Lemma suspended_in_sched_new_is_continuous:
        ∀ t t_mid,
          suspended_in_sched_new any_j t →
          suspension_start sched_new any_j t ≤ t_mid < t →
          suspended_in_sched_new any_j t_mid.

    End SuspensionPredicate.

    Section SuspensionTable.

      Lemma suspended_in_sched_new_only_inside_window:
        ∀ any_j t,
          arr_j + R ≤ t →
          ~~ suspended_at job_arrival inflated_job_cost reduced_suspension_duration
                          sched_new any_j t.

      Lemma sched_new_suspension_matches:
        ∀ any_j t,
          t < arr_j + R →
          suspended_in_sched_new any_j t =
          suspended_at job_arrival inflated_job_cost reduced_suspension_duration sched_new any_j t.

      Let cumulative_suspension_in_sched_susp :=
        cumulative_suspension job_arrival job_cost job_suspension_duration sched_susp.
      Let cumulative_suspension_in_sched_new :=
        cumulative_suspension job_arrival inflated_job_cost reduced_suspension_duration sched_new.

      Lemma sched_new_has_shorter_suspension:
        ∀ any_j t,
          cumulative_suspension_in_sched_new any_j t
          ≤ cumulative_suspension_in_sched_susp any_j t.

      Corollary sched_new_has_shorter_total_suspension:
        ∀ any_j,
          total_suspension inflated_job_cost reduced_suspension_duration any_j ≤
          total_suspension job_cost job_suspension_duration any_j.

    End SuspensionTable.

    Section AdditionalScheduleProperties.

      Lemma sched_new_respects_self_suspensions:
        respects_self_suspensions job_arrival inflated_job_cost reduced_suspension_duration sched_new.

      Lemma sched_new_work_conserving:
        work_conserving job_arrival inflated_job_cost reduced_suspension_duration
                        arr_seq sched_new.

      Lemma sched_new_respects_policy:
        respects_JLDP_policy job_arrival inflated_job_cost reduced_suspension_duration
                             arr_seq sched_new higher_eq_priority.

    End AdditionalScheduleProperties.

    Section FinalRemarks.

      Remark sched_new_is_valid:
        valid_suspension_aware_schedule job_arrival arr_seq higher_eq_priority
                                  reduced_suspension_duration inflated_job_cost sched_new.

      Remark sched_new_response_time_of_job_j:
        job_response_time_in_sched_new_bounded_by j R →
        job_response_time_in_sched_susp_bounded_by j R.

    End FinalRemarks.

  End ReductionProperties.

End SustainabilityAllCostsProperties.