From HB Require Import structures.
[Loading ML file ring_plugin.cmxs (using legacy method) ... done]
[Loading ML file ssrmatching_plugin.cmxs (using legacy method) ... done]
[Loading ML file ssreflect_plugin.cmxs (using legacy method) ... done]
Serlib plugin: coq-elpi.elpi is not available: serlib support is missing.
Incremental checking for commands in this plugin will be impacted.
[Loading ML file coq-elpi.elpi ... done]
Require Export prosa.behavior.all.
[Loading ML file zify_plugin.cmxs (using legacy method) ... done]
[Loading ML file micromega_core_plugin.cmxs (using legacy method) ... done]
[Loading ML file micromega_plugin.cmxs (using legacy method) ... done]
[Loading ML file btauto_plugin.cmxs (using legacy method) ... done]
Notation "_ + _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ - _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ <= _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ < _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ >= _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ > _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ <= _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation "_ < _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation "_ <= _ < _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation "_ < _ < _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation "_ * _" was already used in scope nat_scope.
[notation-overridden,parsing,default]

(** In the following, we define a processor state model for an ideal-uniprocessor
    system with jobs possibly exhibiting exceedance. *)
Section State.

  (** For a give type of jobs ...*)
  Context `{Job : JobType}.

  (** ... the exceedance processor state is defined as follows.
      Here, the [NominalExecution] processor state refers to the state of the
      processor when it is executing some job [j]. [ExceedanceExecution] also
      refers to the state of the processor when a job is executing in addition
      to its nominal execution time. Finally, [Idle] refers to the state of the
      processor when no job is executing. *)
  Inductive exceedance_processor_state :=
  | NominalExecution (j : Job)
  | ExceedanceExecution (j : Job)
  | Idle.

  (** To efficiently use the processor state in our mechanization, we need to
      define an [eqType] for the processor state. First, we define an inequality
      on the processor state as follows. *)
  Definition exceedance_processor_state_eqdef (p1 p2 : exceedance_processor_state) : bool :=
    match p1, p2 with
    | NominalExecution j1, NominalExecution j2 => j1 == j2
    | ExceedanceExecution j1, ExceedanceExecution j2 => j1 == j2
    | Idle, Idle => true
    | _, _ => false
    end.

  (** Next, we prove that the defined notion of equality is in fact an equality. *)
  Lemma eqn_exceedance_processor_state : Equality.axiom exceedance_processor_state_eqdef.
Job: JobType
Equality.axiom (T:=exceedance_processor_state)
  exceedance_processor_state_eqdef
  Proof.
Job: JobType
Equality.axiom (T:=exceedance_processor_state)
  exceedance_processor_state_eqdef
    unfold Equality.axiom.
Job: JobType
forall x y : exceedance_processor_state,
reflect (x = y) (exceedance_processor_state_eqdef x y)
    move => s1 s2.
Job: JobType
s1, s2: exceedance_processor_state
reflect (s1 = s2)
  (exceedance_processor_state_eqdef s1 s2)
    destruct (exceedance_processor_state_eqdef s1 s2) eqn: EQ.
Job: JobType
s1, s2: exceedance_processor_state
EQ: exceedance_processor_state_eqdef s1 s2 = true
reflect (s1 = s2) true
Job: JobType
s1, s2: exceedance_processor_state
EQ: exceedance_processor_state_eqdef s1 s2 = false
reflect (s1 = s2) false
    -
Job: JobType
s1, s2: exceedance_processor_state
EQ: exceedance_processor_state_eqdef s1 s2 = true
reflect (s1 = s2) true apply ReflectT.
Job: JobType
s1, s2: exceedance_processor_state
EQ: exceedance_processor_state_eqdef s1 s2 = true
s1 = s2
      by destruct s1; destruct s2 => //=;  move : EQ => /eqP -> .
    -
Job: JobType
s1, s2: exceedance_processor_state
EQ: exceedance_processor_state_eqdef s1 s2 = false
reflect (s1 = s2) false apply /ReflectF => EQ1.
Job: JobType
s1, s2: exceedance_processor_state
EQ: exceedance_processor_state_eqdef s1 s2 = false
EQ1: s1 = s2
False
      move : EQ => /negP.
Job: JobType
s1, s2: exceedance_processor_state
EQ1: s1 = s2
~ exceedance_processor_state_eqdef s1 s2 -> False apply.
Job: JobType
s1, s2: exceedance_processor_state
EQ1: s1 = s2
exceedance_processor_state_eqdef s1 s2
      by destruct s1; destruct s2 => //=; inversion EQ1; subst.
  Qed.

  (** Finally, we register the processor state as an [eqType]. *)
  HB.instance Definition _ := hasDecEq.Build exceedance_processor_state eqn_exceedance_processor_state.

  (** Next, we need to define the notions of service and supply for the
      processor state under consideration. *)
  Section ExceedanceService.

    (** Consider any job [j]. *)
    Variable j : Job.

    (** [j] is considered to be "scheduled" if the processor state is either
        [NominalExecution j] or [ExceedanceExecution j] *)
    Definition exceedance_scheduled_on (proc_state : exceedance_processor_state) (_ : unit)
      : bool :=
      match proc_state with
      | NominalExecution j'
      | ExceedanceExecution j' => j' == j
      | _ => false
      end.

    (** Next, we need to define in which states the processor is offering supply.
        This is required to specify in which states a processor can offer
        productive work to a job. Note that when analysing a schedule of the
        [exceedance_processor_state], we want to model all instances of
        [ExceedanceExecution] as blackouts w.r.t. to nominal service and, therefore, the supply in this
        processor state is defined to be [0]. *)
    Definition exceedance_supply_on (proc_state :  exceedance_processor_state)
      (_ : unit) : work :=
      match proc_state with
      | NominalExecution _ => 1
      | ExceedanceExecution _ => 0
      | Idle => 1
      end.

    (** Finally we need to define in which states a job actually receives
        nominal service. In our case, a job [j] receives nominal service only when the system
        is in the [NominalExecution j] state. *)
    Definition exceedance_service_on (proc_state : exceedance_processor_state) (_ : unit) : work :=
      match proc_state with
      | NominalExecution j' => j' == j
      | ExceedanceExecution _ => 0
      | Idle => 0
      end.

  End ExceedanceService.

    (** Finally we can declare our processor state as an instance of the
        [ProcessorState] typeclass. *)
    Global Program Instance exceedance_proc_state : ProcessorState Job :=
      {|
        State := exceedance_processor_state;
        scheduled_on := exceedance_scheduled_on;
        supply_on := exceedance_supply_on;
        service_on := exceedance_service_on
      |}.
    Next Obligation.
Job: JobType
forall (j : Job) (s : exceedance_processor_state)
  (r : Datatypes_unit__canonical__fintype_Finite),
exceedance_service_on j s r <=
exceedance_supply_on s r
      by move => j [] // s [] /=; case: eqP; lia.
    Qed.
    Next Obligation.
Job: JobType
forall (j : Job) (s : exceedance_processor_state)
  (r : Datatypes_unit__canonical__fintype_Finite),
~~ exceedance_scheduled_on j s r ->
exceedance_service_on j s r = 0
      by move => j [] // s [] /=; case: eqP; lia.
    Qed.

End State.

Global Arguments exceedance_proc_state : clear implicits.