# Library prosa.analysis.facts.model.cumulative_cost

Require Export prosa.model.task.cumulative_cost.
Require Export prosa.analysis.facts.model.task_arrivals.

# Facts About Cumulative Task Costs

In this file, we establish basic consequences of cumulative task-cost validity. In particular, a cumulative bound for singleton blocks implies the ordinary scalar job-cost validity assumption.
We first establish some basic facts about consecutive arrivals of a task.
Section ConsecutiveArrivals.
Consider any type of tasks and their jobs.
Context {Task : TaskType}.
Context {Job : JobType} `{JobTask Job Task} `{JobArrival Job}.
Consider any job arrival sequence with consistent arrival times.
Variable arr_seq : arrival_sequence Job.
Hypothesis H_consistent_arrivals : consistent_arrival_times arr_seq.
Any arriving job j is trivially a "consecutive" block in the arrival sequence of job_task j.
Lemma arriving_job_is_consecutive_task_arrival :
∀ j,
arrives_in arr_seq j →
consecutive_task_arrivals arr_seq (job_task j) [:: j].
The arrivals of a given task in any half-open interval are consecutive.
Lemma task_arrivals_between_is_consecutive_task_arrival :
∀ tsk t1 t2,
t1 ≤ t2 →
consecutive_task_arrivals arr_seq tsk
(task_arrivals_between arr_seq tsk t1 t2).
End ConsecutiveArrivals.
Next, we derive ordinary scalar job-cost validity from cumulative cost validity.
Section ValidJobCosts.
Consider any type of tasks with cumulative cost bounds ...
Context {Task : TaskType} `{TaskCumulativeCost Task}.
... and their associated jobs with execution costs and arrival times.
Context {Job : JobType} `{JobTask Job Task} `{JobCost Job} `{JobArrival Job}.
Consider any job arrival sequence with consistent arrival times.
Variable arr_seq : arrival_sequence Job.
Hypothesis H_consistent_arrivals : consistent_arrival_times arr_seq.
Let task_cost be defined by WCET(1).
#[local] Existing Instance task_cost_from_cumulative_cost.
Given a task that with a valid cumulative cost bound tsk, every arriving job j of the task has a valid scalar job cost.
Lemma valid_job_cost_from_cumulative_cost_bound :
∀ tsk,
respects_task_cumulative_cost arr_seq tsk →
∀ j,
arrives_in arr_seq j →
job_of_task tsk j →
valid_job_cost j.
We next lift the above property to task sets. Consider any given task set with valid cumulative execution-time bounds.
Variable ts : seq Task.
Hypothesis H_bounds_respected : taskset_respects_cumulative_cost_bounds arr_seq ts.
All jobs in an arrival sequence of the task set have valid scalar job costs.
Corollary valid_job_costs_from_cumulative_cost_bounds :
all_jobs_from_taskset arr_seq ts →
arrivals_have_valid_job_costs arr_seq.
End ValidJobCosts.
The trivial cumulative cost WCET(n) = n × WCET is valid for every task.
Section TrivialCumulativeCostValidity.
Consider any type of tasks with a scalar WCET ...
Context {Task : TaskType} `{ScalarCost : TaskCost Task}.
... and the induced trivial WCET(n) bound for such tasks.
Let TrivialCumulativeCost := (@task_cost_as_cumulative_cost Task ScalarCost).
The trivial cumulative bound induced by the scalar bound is well formed.
Lemma trivial_cumulative_cost_valid :
∀ tsk,
@valid_task_cumulative_cost Task TrivialCumulativeCost tsk.
Next, consider an arrival sequence of the jobs associated with these tasks.
Context {Job : JobType} `{JobTask Job Task} `{JobCost Job} `{JobArrival Job}.
Variable arr_seq : arrival_sequence Job.
Ordinary scalar job-cost validity implies that the induced trivial WCET(n) bound is respected.
Lemma trivial_cumulative_cost_respected :
arrivals_have_valid_job_costs arr_seq →
∀ tsk,
@respects_task_cumulative_cost Task TrivialCumulativeCost
Job _ _ arr_seq tsk.
For automation, we lift the two previous lemmas to task sets.
Variable ts : seq Task.
The induced trivial WCET(n) bound is valid for every task.
Fact taskset_trivial_cumulative_cost_valid :
taskset_has_valid_cumulative_cost_bounds ts.
The induced trivial WCET(n) bound is respected by every task if each task's WCET is valid.
Fact taskset_trivial_cumulative_cost_bound_respected :
arrivals_have_valid_job_costs arr_seq →
taskset_respects_cumulative_cost_bounds arr_seq ts.
End TrivialCumulativeCostValidity.
We add the above lemmas about the induced trivial cost bound into the "Hint Database" basic_rt_facts so that they become available for proof automation.
Global Hint Resolve
valid_job_cost_from_cumulative_cost_bound
valid_job_costs_from_cumulative_cost_bounds
trivial_cumulative_cost_valid
trivial_cumulative_cost_respected
taskset_trivial_cumulative_cost_valid
taskset_trivial_cumulative_cost_bound_respected
: basic_rt_facts.