Library probsa.rt.analysis.WCET_is_pWCET

From probsa.util Require Export bigop_inf.
From probsa.probability Require Export pred.
From probsa.rt.model Require Export task WCET events axiomatic_pWCET .

WCET is Axiomatic pWCET

Section WCETisAxiomaticPWCET.

Consider a probability space (Ω, μ), ...
  Context {Ω} {μ : measure Ω}.

... any type of tasks with costs defined by a function task_cost, ...
  Context {Task : TaskType}
          {task_cost : TaskCost Task}.

... and any finite type of jobs associated with these tasks. Assume that the jobs have probabilistic arrivals and costs defined by job_arrival and job_cost, respectively.
  Context {Job : finType}.
  Context {job_task : JobTask Job Task}
          {job_arrival : JobArrivalRV Job Ω μ}
          {job_cost : JobCostRV Job Ω μ}.

Let us assume that task_cost is a WCET in the system (Ω,μ).
  Hypothesis H_task_cost_is_valid_WCET : task_cost_is_WCET.

Here we state that WCET might be interpreted as a pWCET. For this, we define a degenerate distribution with one step at workload task_cost tsk, which represents the WCET of a task tsk.
  Program Instance WCET_pmf : ProbWCET Task :=
    {|
      pWCET_pmf (tsk : Task) (c : work) := if task_cost tsk == c then 1%R else 0%R
    |}.
  Next Obligation.
    by destruct (_ == _ ); nra.
  Qed.
  Next Obligation.
    eapply is_series_ext.
    { intros n; eapply countable_sum_ext with (f := fun c ⇒ if c == task_cost tsk then 1 else 0) ⇒ n'.
      destruct (_ == _) eqn:EQ1, (task_cost _ == _) eqn:EQ2; (try done); exfalso.
      - by move: EQ1 EQ2 ⇒ /eqP EQ; subst; rewrite eq_refl.
      - by move: EQ2 EQ1 ⇒ /eqP EQ; subst; rewrite eq_refl.
    }
    { by apply bigop_inf.is_seriesC_bump. }
  Qed.

Next, we prove that partition_into_singletons trivially ensures the job_cost_partition_independence. The idea here is that conditioned on a singleton {ω} (for ω ∈ Ω), any random variable becomes a constant. But constants are always independent. Hence, the conditional independence holds.
  Lemma partition_into_singletons_partition_intependent :
    ∀ j ξ,
      job_cost_partition_independence μ j ξ (partition_into_singletons μ).
  Proof.
    intros j ξ ω POS × NIN.
    have EQUIV : ∀ ω0, (xpred1 ω) ω0 = (ξ_fix arr_seq ξ ∩ partition_into_singletons μ◁{ω}) ω0.
    { intros ω'; unfold "∩", pred_intersection in ×.
      case EQ: (ω' == ω).
      { move: EQ ⇒ /eqP EQ; subst ω'.
        apply pr_pos_inv in POS; move: POS ⇒ [ω' [/andP [Pξ EQ] _]].
        move: EQ ⇒ /eqP EQ; subst ω'.
        by rewrite Pξ /partition_into_singletons //= eq_refl.
      }
      { by rewrite /partition_into_singletons //= eq_sym EQ andb_false_r. }
    }
    have POS2 : PosProb μ (xpred1 ω).
    { apply pr_pos_inv in POS; move: POS ⇒ [ω' [/andP [_ EQ] POS]].
      move: EQ ⇒ /eqP EQ; subst ω'.
      by eapply pr_pos; eauto.
    }
    repeat (
        unshelve
          erewrite (@pr_cond_eq_cond
                      _ _ _ (ξ_fix arr_seq ξ ∩ partition_into_singletons μ◁{ω}) (xpred1 ω))
      ); auto.
    by rewrite !pr_cond_xpred1 -indicator_andb_mult; apply: indicator_pred_eq.
  Qed.

Next, we prove that conditioned on a singleton {ω}, any job cost is still bounded by WCET. This follows from the fact that we simply assume WCET is valid. The rest of the proof just connects the probabilistic interpretation of WCET with job costs.
  Lemma partition_into_singletons_partition_dominated :
    ∀ j ξ,
      job_cost_partition_dominated μ j ξ (partition_into_singletons μ).
  Proof.
    intros j ξ ω POS x.
    have EQUIV : ∀ ω0, (xpred1 ω) ω0 = (ξ_fix arr_seq ξ ∩ partition_into_singletons μ◁{ω}) ω0.
    { intros ω'; unfold "∩", pred_intersection in ×.
      case EQ: (ω' == ω).
      { move: EQ ⇒ /eqP EQ; subst ω'.
        apply pr_pos_inv in POS; move: POS ⇒ [ω' [/andP [Pξ EQ] _]].
        move: EQ ⇒ /eqP EQ; subst ω'.
        by rewrite Pξ /partition_into_singletons //= eq_refl.
      }
      { by rewrite /partition_into_singletons //= eq_sym EQ andb_false_r. }
    }
    have POS2 : PosProb μ (xpred1 ω).
    { apply pr_pos_inv in POS; move: POS ⇒ [ω' [/andP [_ EQ] POS]].
      move: EQ ⇒ /eqP EQ; subst ω'.
      by eapply pr_pos; eauto.
    }
    rewrite /cdf_cond.
    unshelve
      erewrite (@pr_cond_eq_cond
                  _ _ _ (ξ_fix arr_seq ξ ∩ partition_into_singletons μ◁{ω}) (xpred1 ω)); auto.
    rewrite pr_cond_xpred1.
    have EQ: pWCET_cdf (job_task j) x = I[(task_cost (job_task j) ≤ x)%nat].
    { rewrite /pWCET_cdf /pWCET_pmf //=.
      destruct (task_cost (job_task j) ≤ x)%N eqn:LE.
      { erewrite SeriesC_ext with (b := fun w ⇒ if w == task_cost (job_task j) then 1 else 0).
        { by rewrite SeriesC_bump. }
        { intros n; rewrite eq_sym; destruct (n == task_cost (job_task j)) eqn:EQ1.
          { by move: EQ1 ⇒ /eqP EQ1; subst; rewrite LE eq_refl. }
          { by rewrite !EQ1; destruct (n ≤ x)%nat. }
        }
      }
      { apply SeriesC_0 ⇒ n.
        destruct (n ≤ x)%nat eqn:LE2, (task_cost (job_task j) == n) eqn:EQ ⇒ //=.
        by move: EQ ⇒ /eqP EQ; subst; rewrite LE2 in LE.
      }
    }
    rewrite EQ; clear EQ.
    apply indicator_pred_impl; apply/implyP ⇒ LE.
    unfold "⟨<=⟩", rvar_nat_pred_leqop.
    eapply leq_trans; last by apply LE.
    by apply H_task_cost_is_valid_WCET.
  Qed.

Since both conditions hold, we can conclude that WCET is an axiomatic pWCET. Note, however, that here we only prove that WCET could be interpreted as an axiomatic pWCET, not that this is the ony possible pWCET.
  Lemma WCET_is_axiomatic_pWCET :
    axiomatic_pWCET μ.
  Proof.
    by intros j ξ; eexists; split;
      [ apply partition_into_singletons_partition_intependent
      | apply partition_into_singletons_partition_dominated].
  Qed.

End WCETisAxiomaticPWCET.