added the np_respect_preemption_model lemma

Proved that np_uni_schedule respects the preemption model

Proved priority compliance of uni_schedule.

implementation/facts/ideal_uni/preemption_aware.v

 Require Export prosa.implementation.facts.generic_schedule.
 Require Export prosa.implementation.definitions.ideal_uni_scheduler.
 Require Export prosa.analysis.facts.model.ideal_schedule.
+Require Export prosa.model.schedule.limited_preemptive.
 
 (** * Properties of the Preemption-Aware Ideal Uniprocessor Scheduler *)
 
@@ -210,6 +211,41 @@ Section NPUniprocessorScheduler.
 
   End PreemptionTimes.
 
+  (** In this section, we establish that the preemption-aware scheduler indeed respects
+      the preemption model semantics. *)
+  Section PreemptionCompliance.
+
+    (** Assuming that every job in [arr_seq] adheres by the rule that jobs must
+        start execution to become nonpreemptive,... *)
+    Hypothesis H_valid_preemption_function : forall j, arrives_in arr_seq j ->
+                                                  job_cannot_become_nonpreemptive_before_execution j.
+
+    (** ...we show that the generated schedule respects the preemption model semantics. *)
+    Lemma np_respects_preemption_model :
+      schedule_respects_preemption_model arr_seq schedule.
+    Proof.
+      rewrite /schedule_respects_preemption_model => j.
+      elim => [| t' IH];
+               first by rewrite service0 => ARR /negP NP; move: (H_valid_preemption_function j ARR) => P; exfalso.
+      move => ARR NP.
+      have SCHED : scheduled_at schedule j t'.
+      { apply contraT => NOT_SCHED.
+        move: (not_scheduled_implies_no_service _ _ _ NOT_SCHED) => NO_SERVICE.
+        rewrite -(service_last_plus_before) NO_SERVICE addn0 in NP; apply IH in NP => //.
+        now move /negP in NOT_SCHED. }
+      rewrite /schedule/np_uni_schedule scheduled_at_def /generic_schedule schedule_up_to_def /allocation_at /prev_job_nonpreemptive.
+      rewrite /schedule /np_uni_schedule scheduled_at_def /generic_schedule /allocation_at in SCHED.
+      move /eqP in SCHED; rewrite SCHED.
+      rewrite (identical_prefix_service _ schedule).
+      rewrite ifT => //.
+      rewrite /identical_prefix /schedule /np_uni_schedule /generic_schedule.
+      move => h LT; rewrite ltnS in LT.
+      now rewrite (schedule_up_to_prefix_inclusion _ _ _ _ LT h).
+    Qed.
+
+
+  End PreemptionCompliance.
+
 End NPUniprocessorScheduler.
 
 

implementation/facts/ideal_uni/prio_aware.v

@@ -119,4 +119,22 @@ Section PrioAwareUniprocessorScheduler.
 
   End Priority.
 
+  (** In this section, we show that [uni_schedule arr_seq] respects the preemption model semantics. *)
+  Section PreemptionCompliance.
+
+    (** Suppose that every job in [arr_seq] adheres by the rule that jobs must
+        start execution to become nonpreemptive. *)
+    Hypothesis H_valid_preemption_function : forall j, arrives_in arr_seq j ->
+                                                  job_cannot_become_nonpreemptive_before_execution j.
+
+    (** Since [uni_schedule arr_seq] is an instance of [np_uni_schedule], then the compliance of
+        [schedule] to the preemption model follows trivially from the compliance of [np_uni_schedule]. *)
+    Lemma schedule_respects_preemption_model :
+      schedule_respects_preemption_model arr_seq schedule.
+    Proof.
+      by apply np_respects_preemption_model .
+    Qed.
+
+  End PreemptionCompliance.
+
 End PrioAwareUniprocessorScheduler.