.ackrc

+# Configuration file for the 'ack' search utility
+# See https://beyondgrep.com/ for details.
+
+# Ignore misc files generated by the build process
+--ignore-file=ext:glob,aux,d,conf,orig
+--ignore-dir=html

.gitattributes

+*.v gitlab-language=coq

.gitignore

 *.d
 *.glob
 *.vo
+*.vos
+*.vok
 *.html
+/html
 *.aux
+Makefile.coq*
+Makefile.conf
+*.crashcoqide
+*.v#
+*.cache
+*~
+*.swp
+*.orig
+*/.#*
+#*#
+.#*
+*.DS_Store
+/proof-state
+/with-proof-state
+/html-alectryon
+_esy
+esy.lock/
+_CoqProject

.gitlab-ci.yml

+###################### Global Config ######################
+
+workflow:
+  rules:
+    - if: '$CI_PIPELINE_SOURCE == "merge_request_event"'
+    - if: '$CI_COMMIT_BRANCH && $CI_OPEN_MERGE_REQUESTS'
+      when: never
+    - if: '$CI_COMMIT_BRANCH'
+
+stages:
+  - build
+
+###################### Rules and Scripts ##################
+
+.not_in_wip_branches:
+  rules:
+    - if: ($CI_COMMIT_BRANCH !~ /^wip-.*$/) || ($CI_PIPELINE_SOURCE == "merge_request_event")
+
+.only_in_wip_branches:
+  rules:
+    - if: ($CI_COMMIT_BRANCH =~ /^wip-.*$/) && ($CI_PIPELINE_SOURCE != "merge_request_event")
+
+.build-common:
+  stage: build
+  script:
+    - opam pin add -n -y -k path coq-prosa .
+    - opam install -y -v -j ${NJOBS} coq-prosa
+    - opam pin add -n -y -k path coq-prosa-refinements .
+    - opam install -y -v -j ${NJOBS} coq-prosa-refinements
+
+.preferred-stable-version:
+    image: registry.mpi-sws.org/mathcomp-for-prosa:2.3.0-coq-8.20
+
+.build:
+  image: registry.mpi-sws.org/mathcomp-for-prosa:${CI_JOB_NAME}
+  extends: .build-common
+
+.build-and-test-POET:
+  extends: .build
+  script:
+    - git clone https://gitlab.mpi-sws.org/RT-PROOFS/POET.git -b POET-for-Prosa-CI-next /tmp/POET
+    - !reference [.build-common, script]
+    - mv /tmp/POET .
+    - cd POET
+    - pip3 install --break-system-packages -r requirements.txt
+    - >-
+      for WORKLOAD in examples/*.yaml;
+      do
+        CERT=certs/cert-for-`basename $WORKLOAD`;
+        echo; echo; echo;
+        echo "==================";
+        echo "Testing $WORKLOAD:";
+        mkdir -p $CERT;
+        time ./poet -v -o $CERT -j ${NJOBS} -s $WORKLOAD;
+      done;
+      
+
+.make-html:
+  script:
+    - make html -j ${NJOBS}
+    - mv html with-proofs
+    - make gallinahtml -j ${NJOBS}
+    - mv html without-proofs
+    - make htmlpretty -j ${NJOBS}
+    - mv html pretty
+
+###################### The Jobs ######################
+
+2.2.0-coq-8.19:
+  extends:
+    - .build
+    - .not_in_wip_branches
+
+2.3.0-coq-8.20:
+  extends:
+    - .build
+    - .not_in_wip_branches
+
+POET:
+  extends:
+    - .build-and-test-POET
+    - .preferred-stable-version
+    - .not_in_wip_branches
+
+compile-and-doc:
+  stage: build
+  extends:
+    - .only_in_wip_branches
+    - .preferred-stable-version
+  script:
+    - make -j ${NJOBS} all
+    - !reference [.make-html, script]
+  artifacts:
+    name: "prosa-spec-$CI_COMMIT_REF_NAME"
+    paths:
+      - "with-proofs/"
+      - "without-proofs/"
+      - "pretty/"
+    expire_in: 1 week
+
+compile-and-doc-and-validate:
+  stage: build
+  extends:
+    - .not_in_wip_branches
+    - .preferred-stable-version
+  script:
+    - make -j ${NJOBS} all 2>&1 | tee coqc-messages.txt
+    - if grep -q Warning coqc-messages.txt; then (echo "Please fix all Coq warnings:"; echo "--"; grep -B1 Warning coqc-messages.txt; exit 1); fi
+    - !reference [.make-html, script]
+    - scripts/check-axiom-free.sh results
+##### `make validate` disabled because of https://github.com/LPCIC/coq-elpi/issues/677 and https://github.com/coq/coq/issues/17345
+#     - make validate 2>&1 | tee validation-results.txt
+#     - scripts/check-validation-output.sh --accept-proof-irrelevance validation-results.txt
+  artifacts:
+    name: "prosa-spec-$CI_COMMIT_REF_NAME"
+    paths:
+      - "with-proofs/"
+      - "without-proofs/"
+      - "pretty/"
+    expire_in: 1 week
+
+mangle-names:
+  stage: build
+  extends:
+    - .not_in_wip_branches
+    - .preferred-stable-version
+  script:
+    - make -j ${NJOBS} mangle-names
+
+# Check that proof irrelevance shows up only due to refinements.
+compile-and-validate:
+  stage: build
+  extends:
+    - .not_in_wip_branches
+    - .preferred-stable-version
+  script:
+    - make -j ${NJOBS}
+    - scripts/check-axiom-free.sh results
+##### `make validate` disabled because of https://github.com/LPCIC/coq-elpi/issues/677 and https://github.com/coq/coq/issues/17345
+#     - make validate 2>&1 | tee validation-results.txt
+#     - scripts/check-validation-output.sh validation-results.txt
+
+proof-length:
+  stage: build
+  image: python:3
+  script:
+    - make proof-length
+
+spell-check:
+  extends:
+    - .not_in_wip_branches
+  stage: build
+  image: registry.mpi-sws.org/aspell-ci:2023-03
+  script:
+    - make spell
+
+# mathcomp-dev with stable Coq
+#coq-8.17:
+#  extends:
+#    - .build-dev
+#    - .not_in_wip_branches
+#  # it's ok to fail with an unreleased version of ssreflect
+#  allow_failure: true
+
+# mathcomp-dev with coq-dev
+#coq-dev:
+#  extends:
+#    - .build-dev
+#    - .not_in_wip_branches
+#  # it's ok to fail with an unreleased version of ssreflect and Coq
+#  allow_failure: true
+
+proof-state:
+  extends:
+   - .not_in_wip_branches
+  stage: build
+  image: registry.mpi-sws.org/alectryon-ci:2.3.0-coq-8.20
+  script:
+    - eval $(opam env)
+    - make -j ${NJOBS} all
+    - make -j ${NJOBS} alectryon
+  artifacts:
+    name: "prosa-proof-state-$CI_COMMIT_REF_NAME"
+    paths:
+      - "html-alectryon/"
+    expire_in: 1 week

.mailmap

+Björn Brandenburg <bbb@mpi-sws.org> Björn Brandenburg <bbb@mpi-sws.org>
+
+Sergey Bozhko <sbozhko@mpi-sws.org> Sergei Bozhko <sbozhko@mpi-sws.org>
+Sergey Bozhko <sbozhko@mpi-sws.org> Sergey Bozhko <gkerfimf@gmail.com>
+Sergey Bozhko <sbozhko@mpi-sws.org> Sergey Bozhko <sbozhko@sws-mpi.org>
+
+Kimaya Bedarkar <kbedarka@mpi-sws.org> Kimaya <f20171026@goa.bits-pilani.ac.in>
+Kimaya Bedarkar <kbedarka@mpi-sws.org> Kimaya Bedarkar <f20171026@goa.bits-pilani.ac.in>
+Kimaya Bedarkar <kbedarka@mpi-sws.org> kbedarka <kbedarka@mpi-sws.org>
+Kimaya Bedarkar <kbedarka@mpi-sws.org> kimaya <f20171026@goa.bits-pilani.ac.in>
+Kimaya Bedarkar <kbedarka@mpi-sws.org> Kimaya <kbedarka@mpi-sws.org>
+
+Marco Maida <mmaida@mpi-sws.org> Marco Maida <>
+Marco Maida <mmaida@mpi-sws.org> mmaida <mmaida@mpi-sws.org>
+
+Mariam Vardishvili <mariamvardishvili@gmail.com> mariamvardishvili <mariamvardishvili@gmail.com>
+Mariam Vardishvili <mariamvardishvili@gmail.com> mariamvardishvili <mvardishvili@mpi-sws.org>
+Mariam Vardishvili <mariamvardishvili@gmail.com> Mariam Vardishvili <mvardishvili@mpi-sws.org>
+
+Maxime Lesourd <maxime.lesourd@inria.fr> Maxime Lesourd <maxime.lesourd@gmail.com>
+Martin Bodin <martin.bodin@inria.fr> Martin Constantino–Bodin <martin.bodin@ens-lyon.org>
+Martin Bodin <martin.bodin@inria.fr> Martin Constantino–Bodin <martin.bodin@inria.fr>
+Pierre Roux <pierre.roux@onera.fr> Pierre Roux <pierre@roux01.fr>
+Pierre Roux <pierre.roux@onera.fr> Pierre Roux <proux@mpi-sws.org>
+Sophie Quinton <sophie.quinton@inria.fr> sophie quinton <squinton@inrialpes.fr>
+Sophie Quinton <sophie.quinton@inria.fr> sophie quinton <sophie.quinton@inria.fr>
+Xiaojie GUO <xiaojie.guo@inria.fr> Xiaojie GUO <gxj0303@loic.inrialpes.fr>
+
+Meenal Gupta <meenalg727@gmail.com> Meenal-27 <80755301+Meenal-27@users.noreply.github.com>

LICENSE

+BSD 2-Clause License
+
+Copyright (c) 2014–2022, The Prosa Project & Contributors
+All rights reserved.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions are met:
+
+* Redistributions of source code must retain the above copyright notice, this
+  list of conditions and the following disclaimer.
+
+* Redistributions in binary form must reproduce the above copyright notice,
+  this list of conditions and the following disclaimer in the documentation
+  and/or other materials provided with the distribution.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
+AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
+IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
+DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE
+FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
+DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR
+SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
+CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,
+OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

Makefile.coq.local

+# Prosa: include pretty documentation targets
+include scripts/coqdocjs/Makefile.coqdocjs
+include scripts/Makefile.alectryon
+
+# Hack to enable esy support:
+#
+# In the esy container, $HOME is hidden, but this causes Coq to complain.
+# We thus include a dummy $HOME value.
+HOME ?= $(DESTDIR)
+export HOME

README.md

-# RT-PROOFS
+# Prosa: Formally Proven Schedulability Analysis
 
-This repository contains the main Coq proof spec & proof development of the RT-PROOFS project.
+This repository contains the main Coq specification & proof development of the [Prosa open-source project](https://prosa.mpi-sws.org), which was launched in 2016.
 
-## Directory Structure
+From 2018–201, Prosa was further developed in the context of the [RT-Proofs research project](https://rt-proofs.inria.fr/) (funded jointly by ANR and DFG, projects ANR-17-CE25-0016 and DFG-391919384, respectively).
 
-The Prosa directory is organized in a hierarchy: while generic, reusable foundations stay in
-the upper levels, definitions for specific analyses should go deeper into the directory tree.
+<center><img alt="RT-Proofs logo" src="http://prosa.mpi-sws.org/figures/rt-proofs-logo.png" width="300px"></center>
 
-### Base Directories
+Prosa continues to be maintained and developed by the MPI-SWS Real-Time Systems group and contributors. Patches and merge requests are very welcome!
 
-Currently, Prosa contains the following base directories:
+## Documentation
 
-- **model/:** Specification of task and scheduler models, as well as generic lemmas related to scheduling.
-	  
-- **analysis/:** Definition, proofs and implementation of schedulability analyses.
+Up-to-date documentation for all branches of the main Prosa repository is available on the Prosa homepage:
 
-- **implementation/:** Instantiation of each schedulability analysis with concrete task and scheduler implementations.
-		       Testing the main theorems in an assumption free environment shows the absence of contradictions.
+- <https://prosa.mpi-sws.org/branches>
 
-### Internal Directories
+## Publications
 
-Within each base directory you can find the different classes of schedulers.
+Please see the [list of publications](https://prosa.mpi-sws.org/publications.html) on the Prosa project's homepage.
 
-- **model/uni:** Uniprocessor scheduling.
-- **model/global:** Global scheduling.
-- **model/partitioned:** Partitioned scheduling.
-- **model/apa:** APA scheduling.
+### Classic Prosa
 
-### Extending Prosa
+All results published prior to 2020 used the "classic" version of Prosa as first presented at ECRTS'16. Classic Prosa has been superseded by this development and is no longer being maintained. Refer to [the `classic-prosa` branch](https://gitlab.mpi-sws.org/RT-PROOFS/rt-proofs/-/tree/classic-prosa) to find this original version of Prosa.
 
-When adding a new model or analysis to Prosa, please extend the corresponding directory.
-For example, the schedulability analysis for global scheduling with release jitter is organized as follows.
 
-- **model/global/jitter:** Definitions and lemmas for global scheduling with release jitter.
-- **analysis/global/jitter:** Analysis for global scheduling with release jitter.
-- **implementation/global/jitter:** Implementation of the concrete scheduler with release jitter. 
+## Directory and Module Structure
+
+The directory and module structure is organized as follows. First, the main parts, of which there are currently six.
+
+- [`behavior`](behavior/): The `behavior` namespace collects basic definitions and properties of system behavior (i.e., it defines Prosa's **trace-based semantics**). There are *no* proofs here. This module is mandatory: *all* results in Prosa rely on the basic trace-based semantics defined in this module.
+- [`model`](model/): The `model` namespace collects all definitions and basic properties of various **system models** (e.g., sporadic tasks, arrival curves, various scheduling policies, etc.). There are only few proofs here. This module contains multiple, mutually exclusive alternatives (e.g., periodic vs. sporadic tasks, uni- vs. multiprocessor models, constrained vs. arbitrary deadlines, etc.), and higher-level results are expected "pick and choose" whatever definitions and assumptions are appropriate. These models are *axiomatic* in the sense that they are collections of hypotheses and not necessarily backed by concrete implementations (but see below).
+- [`analysis`](analysis/): The `analysis` namespace collects all definitions and proof libraries needed to establish **system properties** (e.g., schedulability, response time, etc.). This includes a substantial library of *basic facts* that follow directly from the trace-based semantics or specific modelling assumptions. Virtually all intermediate steps and low-level proofs will be found here.
+- [`results`](results/): The `results` namespace contains all **high-level analysis results**.
+- [`implementation`](implementation/): This module collects concrete implementations of some of the axiomatic models and scheduling policies to which the results apply. These are used to instantiate  (i.e., apply) high-level results in an assumption-free environment for concrete job and task types, which establishes the absence of contradictions in the axiomatic models refined by the implementations.
+- [`implementation.refinements`](implementation/refinements/): The refinements needed by [POET](https://drops.dagstuhl.de/opus/volltexte/2022/16336/) to compute with large numbers, based on [CoqEAL](https://github.com/coq-community/CoqEAL).
+
+
+Furthermore, there are a couple of additional folders and modules.
+
+- [`util`](util/): A collection of miscellaneous "helper" lemmas and tactics. Used throughout the rest of Prosa.
+- [`scripts/`](scripts/): Scripts and supporting resources required for continuous integration and documentation generation.
+
+
+## Side-effects
+
+Importing Prosa changes the behavior of ssreflect's `done` tactic by adding basic lemmas about real-time systems.
+
+```
+Ltac done := solve [ ssreflect.done | eauto 4 with basic_rt_facts ].
+```
+Prosa overwrites the default obligation tactic of Coq with `idtac`. Refer [`util.tactics`](util/tactics.v) for details.
+
+
+## Installation
+
+### With the OCaml Package Manager (`opam`)
+
+Prosa can be installed using [`opam`](https://opam.ocaml.org/) (>= 2.0).
+
+```bash
+opam repo add coq-released https://coq.inria.fr/opam/released
+# or for the dev version (git master): https://coq.inria.fr/opam/extra-dev
+opam update
+opam install coq-prosa
+```
+
+### From Sources with `opam`
+
+OPAM can also be used to install a local checkout. For example, this is done in the CI setup (see `.gitlab-ci.yaml`).
+
+```bash
+opam repo add coq-released https://coq.inria.fr/opam/released
+opam update
+opam pin add -n -y -k path coq-prosa .
+opam install coq-prosa
+```
+
+### From Sources With `esy`
+
+Prosa can be installed using the [`esy`](https://esy.sh/) package manager.
+
+#### Installing `esy`
+
+`esy` itself can typically be installed through `npm`.
+It should look something like this on most `apt`-based systems:
+
+```bash
+sudo apt install npm
+sudo npm install --global esy@latest
+```
+
+#### Installing Prosa
+
+With `esy` in place, it is easy to compile Prosa in one go. To download and compile all of Prosa's dependencies (including Coq), and then to compile Prosa itself, simply issue the command:
+
+```bash
+esy
+```
+
+Note that `esy` uses an internal compilation environment, which is not exported to the current shell.
+To work within this environment, prefix any command with `esy`: for instance `esy coqide` to run your system’s CoqIDE within the right environment.
+Alternatively, `esy shell` opens a shell within its environment.
+
+### Manually From Sources
+
+#### Dependencies
+
+Besides on Coq itself, Prosa depends on
+
+1. the `ssreflect` library of the [Mathematical Components project](https://math-comp.github.io),
+2. the [Micromega support for the Mathematical Components library](https://github.com/math-comp/mczify) provided by `mczify`, and
+3. the [The Coq Effective Algebra Library](https://github.com/coq-community/coqeal) (optional, needed only for POET-related refinements).
+
+These dependencies can be easily installed with OPAM.
+
+```bash
+opam install -y coq-mathcomp-ssreflect coq-mathcomp-zify coq-coqeal
+```
+
+Prosa always tracks the latest stable versions of Coq and ssreflect. We do not maintain compatibility with older versions of either Coq or ssreflect.
+
+#### Compiling Prosa
+
+Assuming all dependencies are available (either via OPAM or compiled from source, see the [Prosa setup instructions](http://prosa.mpi-sws.org/setup-instructions.html)), compiling Prosa can be done by just typing:
+
+```bash
+make -j
+```
+
+Depending on how powerful your machine is, this will take a few minutes.
+
+The library can then be installed with:
+
+```bash
+make install
+```
+
+To compile the POET-related refinements (which require CoqEAL to be installed and inject a dependency on the *proof irrelevance* axiom), first install the main Prosa library with the two commands above, then type:
+
+```bash
+make refinements
+```
+
+The newly compiled files can then be installed with:
+
+```bash
+make install
+```
+
+## Generating HTML Documentation
+
+Once the has been library compiled, the `coqdoc` documentation (as shown on the [web page](http://prosa.mpi-sws.org/documentation.html)) can be easily generated with:
+
+- `make htmlpretty -j`  --- pretty documentation based on CoqdocJS (can hide/show proofs),
+- `make gallinahtml -j` --- just the specification, without proofs,
+- `make html -j`  --- full specification with all proofs.
+
+
+Since `coqdoc` requires object files (`*.vo`) as input, please make sure that the code compiles.
 
 ## Commit and Development Rules
 
+We very much welcome external contributions. Please don't hesitate to [get in touch](http://prosa.mpi-sws.org/get-in-touch.html)!
+
+To make things as smooth as possible, here are a couple of rules and guidelines that we seek to abide by.
+
 1. Always follow the project [coding and writing guidelines](doc/guidelines.md).
 
-2. Make sure the master branch "compiles" at each commit. This is not true for the early history of the repository, but going forward we should strive to keep it working at all times. 
+2. Make sure the master branch "compiles" at each commit. This is not true for the early history of the repository, and during certain stretches of heavy refactoring, but going forward we should strive to keep it working at all times.
+
+3. It's okay (and even recommended) to develop in a (private) dirty branch, but please clean up and re-base your branch (i.e., `git-rebase -i`) on top of the current master branch before opening a merge request.
+
+4. Create merge requests liberally. No improvement is too small or too insignificant for a merge request. This applies to documentation fixes (e.g., typo fixes, grammar fixes, clarifications, etc.)  as well.
 
-3. It's ok to develop in a (private) dirty branch, but then clean up and `git-rebase -i` on top of the current master before merging your work into master.
+5. If you are unsure whether a proposed change is even acceptable or the right way to go about things, create a work-in-progress (WIP) merge request as a basis for discussion. A WIP merge request is prefixed by "WIP:" or "Draft:".
 
-4. It's usually a good idea to ask first on the mailing list before merging a substantial change.
+6. We strive to have only "fast-forward merges" without merge commits, so always re-base your branch to linearize the history before merging. (WIP branches do not need to be linear.)
 
-5. Pushing fixes, small improvements, etc. is always ok. 
+7. Recommendation: Document the tactics that you use in the [list of tactics](doc/tactics.md), especially when introducing/using non-standard tactics.
 
-6. Document the tactics that you use in the [list of tactics](doc/tactics.md).
+8. If something seems confusing, please help with improving the documentation. :-)
 
-7. Whenever you have time available, please help with extending the documentation. :-)
\ No newline at end of file
+9. If you don't know how to fix or improve something, or if you have an open-ended suggestion in need of discussion, please file a ticket.

_CoqProject

--R . rt
\ No newline at end of file

analysis/README.md

+# Prosa Analysis Library
+
+This module provides virtually all **analysis concepts and definitions** and encapsulates the bulk of the **intermediate proofs** in Prosa. 
+
+More precisely, this module collects all definitions that are not needed to define the behavioral semantics (found in [`prosa.behavior`](../behavior)) and that also do not conceptually form part of the task and system model (found in [`prosa.model`](../model)). For example, precise notions of "schedulability," "busy window," or "response time" are clearly analysis concepts and consequently defined here. 
+
+The proofs found in this module are "intermediate proofs" in the sense that they are not an end in of themselves; rather, they are a means to enable the proofs of the high-level results provided in the [`prosa.results`](../results) module.
+
+## Structure
+
+The Prosa analysis library is currently organized as follows:
+
+- [`abstract`](./abstract): This provides **abstract RTA** analysis framework, a general and extensible approach to response-time analysis (RTA).
+- [`definitions`](./definitions): This folder currently collects all major and minor **analysis definitions** (such as schedulability, priority inversion, etc.).
+- [`transform`](./transform): This folder contains procedures for transforming schedules, to be used in proofs that rely on modifying a given reference schedule in some way (e.g., the EDF "swapping argument").
+- [`facts`](./facts): Currently the home of virtually all **intermediate proofs**. In particular, [facts.behavior](./facts/behavior) provides a library of basic facts that follow (mostly) directly from Prosa's trace semantics (as given in [`prosa.behavior`](../behavior)).
+
+**NB**: It is expected that the analysis module will be further (re)organized and (re)structured in future versions of Prosa.
+
+## Guidelines
+
+- As a general rule, keep definitions and proofs separate, so that casual readers may read and understand the Prosa specification without encountering intermediate lemmas and proofs. 
+- Prefer folders with many short files over fewer, longer files. 
+- In each file that is specific to some system model, explicitly `Require` the specific modules that jointly constitute the assumed system model (e.g., `Require prosa.model.processor.ideal` to express that the results in a file depend on the ideal-uniprocessor assumption).
\ No newline at end of file

analysis/abstract/IBF/supply.v

+Require Export prosa.analysis.abstract.abstract_rta.
+
+(** In this module, we define _intra-supply interference_ as a kind of
+    conditional interference and use it to define an _intra-supply_
+    interference-bound function ([intra_IBF]). Recall that an
+    interference-bound function is a function that bounds the
+    interference experienced by a job of a task under analysis. This
+    way, the function [intra_IBF] bounds the cumulative interference
+    ignoring the interference due to a lack of supply.
+
+    Here, the term "intra-supply" is inspired by (but not limited to)
+    reservation-based schedulers, where a job only receives service
+    within a corresponding reservation. Similarly, intra-supply
+    interference refers to interference that occurs "inside" the time
+    instances where supply is present. *)
+Section IntraInterferenceBound.
+
+  (** Consider any type of job associated with any type of tasks ... *)
+  Context {Job : JobType}.
+  Context {Task : TaskType}.
+  Context `{JobTask Job Task}.
+
+  (** ... with arrival times and costs. *)
+  Context `{JobArrival Job}.
+  Context `{JobCost Job}.
+
+  (** Consider any kind of processor state model. *)
+  Context {PState : ProcessorState Job}.
+
+  (** Consider any arrival sequence ... *)
+  Variable arr_seq : arrival_sequence Job.
+
+  (** ... and any schedule of this arrival sequence. *)
+  Variable sched : schedule PState.
+
+  (** Let [tsk] be any task that is to be analyzed. *)
+  Variable tsk : Task.
+
+  (** Assume we are provided with abstract functions for interference
+      and interfering workload. *)
+  Context `{Interference Job}.
+  Context `{InterferingWorkload Job}.
+
+  (** Next, we introduce the notions of _intra-supply_ interference
+      and intra-supply IBF. Using these notions, one can separate the
+      interference due to the lack of supply from all the other
+      sources of interference. *)
+
+  (** We define intra-supply interference as interference conditioned
+      on the fact that there is supply. That is, a job [j] experiences
+      intra-supply interference at a time instant [t] if [j]
+      experiences interference at time [t] _and_ there is supply at
+      [t]. *)
+  Definition intra_interference (j : Job) (t : instant) :=
+    cond_interference (fun j t => has_supply sched t) j t.
+
+  (** We define the cumulative intra-supply interference. *)
+  Definition cumul_intra_interference j t1 t2 :=
+    cumul_cond_interference (fun j t => has_supply sched t) j t1 t2.
+
+  (** Consider an interference bound function [intra_IBF]. *)
+  Variable intra_IBF : duration -> duration -> work.
+
+  (** We say that intra-supply interference is bounded by [intra_IBF]
+      iff, for any job [j] of task [tsk], cumulative _intra-supply_
+      interference within the interval <<[t1, t1 + R)>> is bounded by
+      [intra_IBF(A, R)].*)
+  Definition intra_interference_is_bounded_by :=
+    cond_interference_is_bounded_by
+      arr_seq sched tsk intra_IBF
+      (relative_arrival_time_of_job_is_A sched) (fun j t => has_supply sched t).
+
+End IntraInterferenceBound.

analysis/abstract/IBF/supply_task.v

+Require Export prosa.analysis.abstract.abstract_rta.
+Require Export prosa.analysis.abstract.IBF.supply.
+Require Export prosa.analysis.abstract.IBF.task.
+
+(** In this module, we define a _task-intra-supply_-interference-bound
+    function ([task_intra_IBF]). Function [task_intra_IBF] bounds
+    interference ignoring interference due to lack of supply _and_ due
+    to self-interference. *)
+Section TaskIntraInterferenceBound.
+
+  (** Consider any type of job associated with any type of tasks ... *)
+  Context {Job : JobType}.
+  Context {Task : TaskType}.
+  Context `{JobTask Job Task}.
+
+  (** ... with arrival times and costs. *)
+  Context `{JobArrival Job}.
+  Context `{JobCost Job}.
+
+  (** Consider any kind of processor state model. *)
+  Context {PState : ProcessorState Job}.
+
+  (** Consider any arrival sequence ... *)
+  Variable arr_seq : arrival_sequence Job.
+
+  (** ... and any schedule of this arrival sequence. *)
+  Variable sched : schedule PState.
+
+  (** Let [tsk] be any task that is to be analyzed. *)
+  Variable tsk : Task.
+
+  (** Assume we are provided with abstract functions characterizing
+      interference and interfering workload. *)
+  Context `{Interference Job}.
+  Context `{InterferingWorkload Job}.
+
+  (** Next, we introduce the notions of "task intra-supply
+      interference" and "task intra-supply IBF". Using these notions,
+      one can separate the interference due to the lack of supply or
+      due to self-interference from all the other sources of
+      interference. *)
+
+  (** Let us define a predicate stating that (1) there is supply at
+      time [t] and (2) the task of a job [j] is _not_ scheduled at a
+      time instant [t]. *)
+  Definition nonself_intra (j : Job) (t : instant) :=
+    (nonself arr_seq sched j t) && has_supply sched t.
+
+  (** We define _task intra-supply interference_ as interference
+      conditioned on the fact that there is supply and there is no
+      self-interference. *)
+  Definition task_intra_interference (j : Job) (t : instant) :=
+    cond_interference nonself_intra j t.
+
+  (** Consider an interference bound function [task_intra_IBF]. *)
+  Variable task_intra_IBF : duration -> duration -> work.
+
+  (** We say that task intra-supply interference is bounded by
+      [task_intra_IBF] iff, for any job [j] of task [tsk], the
+      cumulative task intra-supply interference within the interval
+      <<[t1, t1 + R)>> is bounded by [task_intra_IBF(A, R)]. *)
+  Definition task_intra_interference_is_bounded_by :=
+    cond_interference_is_bounded_by
+      arr_seq sched tsk task_intra_IBF
+      (relative_arrival_time_of_job_is_A sched) nonself_intra.
+
+End TaskIntraInterferenceBound.

analysis/abstract/definitions.v

+Require Export prosa.model.task.concept.
+
+(** * Definitions for Abstract Response-Time Analysis *)
+
+(** In the following, we propose a set of definitions for the general
+    framework for response-time analysis (RTA) of uni-processor
+    scheduling of real-time tasks with arbitrary arrival models. *)
+
+(** We are going to introduce two main variables of the analysis:
+    (a) interference, and (b) interfering workload. *)
+
+(** ** a) Interference *)
+(** Execution of a job may be postponed by the environment and/or the
+    system due to different factors (preemption by higher-priority
+    jobs, jitter, black-out periods in hierarchical scheduling, lack
+    of budget, etc.), which we call interference.
+
+    Besides, note that even the subsequent activation of a task can
+    suffer from interference at the beginning of its busy interval
+    (despite the fact that this job hasn’t even arrived at that
+    moment!). Thus, it makes more sense (at least for the current
+    busy-interval analysis) to think about interference of a job as
+    any interference within the corresponding busy interval, and not
+    just after the release of the job.
+
+    Based on that rationale, assume a predicate that expresses whether a job [j]
+    under consideration incurs interference at a given time [t] (in
+    the context of the schedule under consideration).  This will be
+    used later to upper-bound job [j]'s response time. Note that a
+    concrete realization of the function may depend on the schedule,
+    but here we do not require this for the sake of simplicity and
+    generality. *)
+Class Interference (Job : JobType) :=
+  interference : Job -> instant -> bool.
+
+(** ** b) Interfering Workload *)
+(** In addition to interference, the analysis assumes that at any time
+    [t], we know an upper bound on the potential cumulative
+    interference that can be incurred in the future by any job (i.e.,
+    the total remaining potential delays). Based on that, assume a
+    function [interfering_workload] that indicates for any job [j], at
+    any time [t], the amount of potential interference for job [j]
+    that is introduced into the system at time [t]. This function will
+    be later used to upper-bound the length of the busy window of a
+    job.  One example of workload function is the "total cost of jobs
+    that arrive at time [t] and have higher-or-equal priority than job
+    [j]". In some task models, this function expresses the amount of the
+    potential interference on job [j] that "arrives" in the system at
+    time [t]. *)
+Class InterferingWorkload (Job : JobType) :=
+  interfering_workload : Job -> instant -> duration.
+
+(** Next we introduce all the abstract notions required by the analysis. *)
+Section AbstractRTADefinitions.
+
+  (** Consider any type of job associated with any type of tasks... *)
+  Context {Job : JobType}.
+  Context {Task : TaskType}.
+  Context `{JobTask Job Task}.
+
+  (** ... with arrival times and costs. *)
+  Context `{JobArrival Job}.
+  Context `{JobCost Job}.
+
+  (** Consider any kind of processor state model. *)
+  Context {PState : ProcessorState Job}.
+
+  (** Consider any arrival sequence ... *)
+  Variable arr_seq : arrival_sequence Job.
+
+  (** ... and any schedule of this arrival sequence. *)
+  Variable sched : schedule PState.
+
+  (** Let [tsk] be any task that is to be analyzed *)
+  Variable tsk : Task.
+
+  (** Assume we are provided with abstract functions for interference
+      and interfering workload. *)
+  Context `{Interference Job}.
+  Context `{InterferingWorkload Job}.
+
+  (** In order to perform subsequent abstract Response Time Analyses
+      (RTAs), it is essential that we have the capability to bound
+      interference of a certain type (for example, interference that
+      comes from other tasks' jobs). To achieve this, we define
+      "conditional" interference as a conjunction of a predicate [P :
+      Job -> instant -> bool] encoding the property of interest and
+      [interference]. *)
+  Definition cond_interference P j t :=
+    (P j t) && (interference j t).
+
+  (** In order to bound the response time of a job, we must consider
+      (1) the cumulative conditional interference, ... *)
+  Definition cumul_cond_interference P j t1 t2 :=
+    \sum_(t1 <= t < t2) cond_interference P j t.
+
+  (**  ... (2) cumulative interference, ... *)
+  Definition cumulative_interference j t1 t2 :=
+    cumul_cond_interference (fun _ _ => true) j t1 t2.
+
+  (** ... and (3) cumulative interfering workload. *)
+  Definition cumulative_interfering_workload j t1 t2 :=
+    \sum_(t1 <= t < t2) interfering_workload j t.
+
+  (** Next, we introduce a notion of absence of speculative
+      execution. This notion is _not_ directly related to Abstract
+      RTA, but it is useful when proving the existence of bounded busy
+      intervals.
+
+      We say that the functions [Interference] and
+      [InterferingWorkload] do not allow speculative execution if the
+      cumulative interference never exceeds the cumulative interfering
+      workload. Intuitively, one can interpret this definition as
+      stating that it is not allowed to perform work before it is
+      known whether it is actually needed (i.e., before the work
+      appears as actual workload). *)
+  Definition no_speculative_execution :=
+    forall j t,
+      cumulative_interference j 0 t <= cumulative_interfering_workload j 0 t.
+
+  (** Definition of Busy Interval *)
+  (** Further analysis will be based on the notion of a busy
+      interval. The overall idea of the busy interval is to take into
+      account the workload that cause a job under consideration to
+      incur interference. In this section, we provide a definition of
+      an abstract busy interval. *)
+  Section BusyInterval.
+
+    (** We say that time instant [t] is a quiet time for job [j] iff
+        two conditions hold. First, the cumulative interference at
+        time [t] must be equal to the cumulative interfering
+        workload. Intuitively, this condition indicates that the
+        potential interference seen so far has been fully "consumed"
+        (i.e., there is no more higher-priority work or other kinds of
+        delay pending). Second, job [j] cannot be pending at any time
+        earlier than [t] _and_ at time instant [t] (i.e., either it
+        was pending earlier but is no longer pending now, or it was
+        previously not pending and may or may not be released
+        now). The second condition ensures that the busy window
+        captures the execution of job [j]. *)
+    Definition quiet_time (j : Job) (t : instant) :=
+      (cumulative_interference j 0 t == cumulative_interfering_workload j 0 t)
+      && ~~ pending_earlier_and_at sched j t.
+
+    (** Based on the definition of quiet time, we say that an interval
+        <<[t1, t2)>> is a (potentially unbounded) busy-interval prefix
+        w.r.t. job [j] iff the interval (a) contains the arrival of
+        job j, (b) starts with a quiet time and (c) remains
+        non-quiet. *)
+    Definition busy_interval_prefix (j : Job) (t1 t2 : instant) :=
+      t1 <= job_arrival j < t2 /\
+      quiet_time j t1 /\
+      (forall t, t1 < t < t2 -> ~ quiet_time j t).
+
+    (** Next, we say that an interval <<[t1, t2)>> is a busy interval
+        iff <<[t1, t2)>> is a busy-interval prefix and [t2] is a quiet
+        time. *)
+    Definition busy_interval (j : Job) (t1 t2 : instant) :=
+      busy_interval_prefix j t1 t2 /\
+      quiet_time j t2.
+
+    (** Note that the busy interval, if it exists, is unique. *)
+    Fact busy_interval_is_unique :
+      forall j t1 t2 t1' t2',
+        busy_interval j t1 t2 ->
+        busy_interval j t1' t2' ->
+        t1 = t1' /\ t2 = t2'.
+    Proof.
+      move=> j t1 t2 t1' t2' BUSY BUSY'.
+      have EQ: t1 = t1'.
+      { apply/eqP.
+        apply/negPn/negP; intros CONTR.
+        move: BUSY => [[IN [QT1 NQ]] _].
+        move: BUSY' => [[IN' [QT1' NQ']] _].
+        move: CONTR; rewrite neq_ltn; move => /orP [LT|GT].
+        { apply NQ with t1' => //; clear NQ.
+          apply/andP; split=> [//|].
+          move: IN IN' => /andP [_ T1] /andP [T2 _].
+            by apply leq_ltn_trans with (job_arrival j).
+        }
+        { apply NQ' with t1 => [|//]; clear NQ'.
+          apply/andP; split=> [//|].
+          move: IN IN' => /andP [T1 _] /andP [_ T2].
+          by apply leq_ltn_trans with (job_arrival j).
+        }
+      }
+      subst t1'.
+      have EQ: t2 = t2'.
+      { apply/eqP.
+        apply/negPn/negP; intros CONTR.
+        move: BUSY => [[IN [_ NQ]] QT2].
+        move: BUSY' => [[IN' [_ NQ']] QT2'].
+        move: CONTR; rewrite neq_ltn; move => /orP [LT|GT].
+        { apply NQ' with t2 => //; clear NQ'.
+          apply/andP; split=> [|//].
+          move: IN IN' => /andP [_ T1] /andP [T2 _].
+          by apply leq_ltn_trans with (job_arrival j).
+        }
+        { apply NQ with t2' => //; clear NQ.
+          apply/andP; split=> [|//].
+          move: IN IN' => /andP [T1 _] /andP [_ T2].
+          by apply leq_ltn_trans with (job_arrival j).
+        }
+      }
+      by subst t2'.
+    Qed.
+
+  End BusyInterval.
+
+  (** In this section, we introduce some assumptions about the busy
+      interval that are fundamental to the analysis. *)
+  Section BusyIntervalProperties.
+
+    (** We say that a schedule is "work-conserving" (in the abstract
+        sense) iff, for any job [j] from task [tsk] and at any time [t]
+        within a busy interval, there are only two options: either (a)
+        [interference(j, t)] holds or (b) job [j] is scheduled at time
+        [t]. *)
+    Definition work_conserving :=
+      forall j t1 t2 t,
+        arrives_in arr_seq j ->
+        job_cost j > 0 ->
+        busy_interval_prefix j t1 t2 ->
+        t1 <= t < t2 ->
+        ~ interference j t <-> receives_service_at sched j t.
+
+    (** Next, we say that busy intervals of task [tsk] are bounded by
+        [L] iff, for any job [j] of task [tsk], there exists a busy
+        interval with length at most [L]. Note that the existence of
+        such a bounded busy interval is not guaranteed if the schedule
+        is overloaded with work.  Therefore, in the later concrete
+        analyses, we will have to introduce an additional condition
+        that prevents overload. *)
+    Definition busy_intervals_are_bounded_by L :=
+      forall j,
+        arrives_in arr_seq j ->
+        job_of_task tsk j ->
+        job_cost j > 0 ->
+        exists t1 t2,
+          t1 <= job_arrival j < t2 /\
+          t2 <= t1 + L /\
+          busy_interval j t1 t2.
+
+    (** Although we have defined the notion of cumulative
+        (conditional) interference of a job, it cannot be used in a
+        (static) response-time analysis because of the dynamic
+        variability of job parameters. To address this issue, we
+        define the notion of an interference bound. *)
+
+    (** As a first step, we introduce a notion of an "interference
+        bound function" [IBF]. An interference bound function is any
+        function with a type [duration -> duration -> work] that bounds
+        cumulative conditional interference of a job of task [tsk] (a
+        precise definition will be presented below).
+
+        Note that the function has two parameters. The second
+        parameter is the length of an interval in which the
+        interference is supposed to be bounded. It is quite intuitive;
+        so, we will not explain it in more detail. However, the first
+        parameter deserves more thoughtful explanation, which we
+        provide next. *)
+    Variable IBF : duration -> duration -> work.
+
+    (** The first parameter of [IBF] allows one to organize a case
+        analysis over a set of values that are known only during the
+        computation. For example, the most common parameter is the
+        relative arrival time [A] of a job (of a task under
+        analysis). Strictly speaking, [A] is not known when computing
+        a fixpoint; however, one can consider a set of [A] that covers
+        all the relevant cases. There can be other valid properties
+        such as "a time instant when a job under analysis has received
+        enough service to become non-preemptive."
+
+        To make the first parameter customizable, we introduce a
+        predicate [ParamSem : Job -> instant -> Prop] that is used to
+        assign meaning to the second parameter. More precisely,
+        consider an expression [IBF(X, delta)], and assume that we
+        instantiated [ParamSem] as some predicate [P]. Then, it is
+        assumed that [IBF(X, delta)] bounds (conditional) interference
+        of a job under analysis [j ∈ tsk] if [P j X] holds. *)
+    Variable ParamSem : Job -> nat -> Prop.
+
+    (** As mentioned, [IBF] must upper-bound the cumulative
+        _conditional_ interference. This is done to make further
+        extensions of the base aRTA easier. The most general aRTA
+        assumes that an IBF bounds _all_ interference of a given job
+        [j]. However, as we refine the model under analysis, we split
+        the IBF into more and more parts. For example, assuming that
+        tasks are sequential, it is possible to split IBF into two
+        parts: (1) the part that upper-bounds the cumulative
+        interference due to self-interference and (2) the part that
+        upper-bounds the cumulative interference due to all other
+        reasons. To avoid duplication, we parameterize the definition
+        of an IBF by a predicate that encodes the type of interference
+        that must be upper-bounded. *)
+    Variable Cond : Job -> instant -> bool.
+
+    (** Next, let us define this reasoning formally. We say that the
+        conditional interference is bounded by an "interference bound
+        function" [IBF] iff for any job [j] of task [tsk] and its busy
+        interval <<[t1, t2)>> the cumulative conditional interference
+        incurred by [j] w.r.t. predicate [Cond] in the sub-interval
+        <<[t1, t1 + Δ)>> does not exceed [IBF(X, Δ)], where [X] is a
+        constant that satisfies a predefined predicate [ParamSem].
+
+        In other words, for a job [j ∈ tsk], the term [IBF(X, Δ)]
+        provides an upper-bound on the cumulative conditional
+        interference (w.r.t. the predicate [Cond]) that [j] might
+        experience in an interval of length [Δ] _assuming_ that
+        [ParamSem j X] holds. *)
+    Definition cond_interference_is_bounded_by :=
+      (** Consider a job [j] of task [tsk], a busy interval <<[t1,
+          t2)>> of [j], and an arbitrary interval <<[t1, t1 + Δ) ⊆
+          [t1, t2)>>. *)
+      forall t1 t2 Δ j,
+        arrives_in arr_seq j ->
+        job_of_task tsk j ->
+        busy_interval j t1 t2 ->
+        (** We require the IBF to bound the interference only within
+           the interval [t1, t1 + Δ). *)
+        t1 + Δ < t2 ->
+        (** Next, we require the [IBF] to bound the interference only
+            until the job is completed, after which the function can
+            behave arbitrarily. *)
+        ~~ completed_by sched j (t1 + Δ) ->
+        (** And finally, the IBF function might depend not only on the
+            length of the interval, but also on a constant [X]
+            satisfying predicate [Param]. *)
+        forall X,
+          ParamSem j X ->
+          cumul_cond_interference Cond j t1 (t1 + Δ) <= IBF X Δ.
+
+  End BusyIntervalProperties.
+
+  (** As an important special case, we say that a job's interference
+      is (unconditionally) bounded by [IBF] if it is conditionally
+      bounded with [Cond := fun j t => true]. *)
+  Definition job_interference_is_bounded_by IBF Param :=
+    cond_interference_is_bounded_by IBF Param (fun _ _ => true).
+
+End AbstractRTADefinitions.

analysis/abstract/ideal/abstract_rta.v

+Require Export prosa.analysis.facts.model.ideal.schedule.
+Require Export prosa.analysis.definitions.schedulability.
+Require Export prosa.analysis.abstract.search_space.
+Require Export prosa.analysis.abstract.abstract_rta.
+Require Export prosa.analysis.abstract.iw_auxiliary.
+
+(** * Abstract Response-Time Analysis For Processor State with Ideal Uni-Service Progress Model *)
+(** In this module, we present an instantiation of the general
+    response-time analysis framework for models that satisfy the ideal
+    uni-service progress assumptions. *)
+
+(** We prove that the maximum (with respect to the set of offsets)
+    among the solutions of the response-time bound recurrence is a
+    response-time bound for [tsk]. Note that in this section we add
+    additional restrictions on the processor state. These assumptions
+    allow us to eliminate the second equation from [aRTA+]'s
+    recurrence since jobs experience no delays while executing
+    non-preemptively. *)
+Section AbstractRTAIdeal.
+
+  (** Consider any type of tasks ... *)
+  Context {Task : TaskType}.
+  Context `{TaskCost Task}.
+  Context `{TaskRunToCompletionThreshold Task}.
+
+  (**  ... and any type of jobs associated with these tasks. *)
+  Context {Job : JobType}.
+  Context `{JobTask Job Task}.
+  Context `{JobArrival Job}.
+  Context `{JobCost Job}.
+  Context `{JobPreemptable Job}.
+
+  (** Consider any kind of uni-service ideal processor state model. *)
+  Context `{PState : ProcessorState Job}.
+  Hypothesis H_ideal_progress_proc_model : ideal_progress_proc_model PState.
+  Hypothesis H_unit_service_proc_model : unit_service_proc_model PState.
+
+  (** Consider any arrival sequence with consistent, non-duplicate arrivals. *)
+  Variable arr_seq : arrival_sequence Job.
+  Hypothesis H_valid_arrival_sequence : valid_arrival_sequence arr_seq.
+
+  (** Next, consider any schedule of this arrival sequence... *)
+  Variable sched : schedule PState.
+  Hypothesis H_jobs_come_from_arrival_sequence:
+    jobs_come_from_arrival_sequence sched arr_seq.
+
+  (** ... where jobs do not execute before their arrival nor after completion. *)
+  Hypothesis H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched.
+  Hypothesis H_completed_jobs_dont_execute : completed_jobs_dont_execute sched.
+
+  (** Assume that the job costs are no larger than the task costs. *)
+  Hypothesis H_valid_job_cost : arrivals_have_valid_job_costs arr_seq.
+
+  (** Consider a task set [ts]... *)
+  Variable ts : list Task.
+
+  (** ... and a task [tsk] of [ts] that is to be analyzed. *)
+  Variable tsk : Task.
+  Hypothesis H_tsk_in_ts : tsk \in ts.
+
+  (** Consider a valid preemption model... *)
+  Hypothesis H_valid_preemption_model :
+    valid_preemption_model arr_seq sched.
+
+  (** ...and a valid task run-to-completion threshold function. That
+      is, [task_rtc tsk] is (1) no bigger than [tsk]'s cost and (2)
+      for any job [j] of task [tsk] [job_rtct j] is bounded by
+      [task_rtct tsk]. *)
+  Hypothesis H_valid_run_to_completion_threshold :
+    valid_task_run_to_completion_threshold arr_seq tsk.
+
+  (** Assume we are provided with abstract functions for Interference
+      and Interfering Workload. *)
+  Context `{Interference Job}.
+  Context `{InterferingWorkload Job}.
+
+  (** We assume that the scheduler is work-conserving. *)
+  Hypothesis H_work_conserving : work_conserving arr_seq sched.
+
+  (** Let [L] be a constant that bounds any busy interval of task [tsk]. *)
+  Variable L : duration.
+  Hypothesis H_busy_interval_exists :
+    busy_intervals_are_bounded_by arr_seq sched tsk L.
+
+  (** Next, assume that [interference_bound_function] is a bound on
+      the interference incurred by jobs of task [tsk] parametrized by
+      the relative arrival time [A]. *)
+  Variable interference_bound_function : (* A *) duration -> (* Δ *) duration -> duration.
+  Hypothesis H_job_interference_is_bounded :
+    job_interference_is_bounded_by
+      arr_seq sched tsk interference_bound_function (relative_arrival_time_of_job_is_A sched).
+
+  (** To apply the generalized aRTA, we have to instantiate [IBF_P]
+      and [IBF_NP]. In this file, we assume we are given a generic function
+      [interference_bound_function] that bounds interference of jobs
+      of tasks in [ts] and which have to be instantiated in subsequent
+      files. We use this function to instantiate [IBF_P]. *)
+
+  (** However, we still have to instantiate function [IBF_NP], which
+      is a function that bounds interference in a non-preemptive stage
+      of execution. We prove that this function can be instantiated
+      with a constant function [λ F Δ ⟹ F - task_rtct tsk]. *)
+  Let IBF_NP (F : duration) (Δ : duration) := F - task_rtct tsk.
+
+  (** Let us re-iterate on the intuitive interpretation of this
+      function. Since [F] is a solution to the first equation
+      [task_rtct tsk + IBF_P tsk A F <= F], we know that by time
+      instant [t1 + F] a job receives [task_rtct tsk] units of service
+      and, hence, it becomes non-preemptive. Given this information,
+      how can we bound the job's interference in an interval <<[t1, t1
+      + R)>>? Note that this interval starts with the beginning of the
+      busy interval. We know that the job receives [F - task_rtct tsk]
+      units of interference, and there will no more
+      interference. Hence, [IBF_NP tsk F Δ := F - task_rtct tsk]. *)
+  Lemma nonpreemptive_interference_is_bounded :
+    job_interference_is_bounded_by
+      arr_seq sched tsk IBF_NP (relative_time_to_reach_rtct sched tsk interference_bound_function).
+  Proof.
+    move => t1 t2 Δ j ARR TSK BUSY LT NCOM F RTC; specialize (RTC _ _ BUSY).
+    have POS : 0 < job_cost j.
+    { move_neq_up ZE; move: ZE; rewrite leqn0; move => /eqP ZE.
+      move: NCOM => /negP NCOM; apply: NCOM.
+      by rewrite /completed_by ZE.
+    }
+    move: (BUSY) => [PREF _].
+    move : (TSK) (BUSY) RTC => /eqP TSKeq [[/andP [LE1 LE2] [QT1 AQT]] QT2] [LEQ RTC].
+    rewrite leq_subRL_impl // addnC -/cumulative_interference.
+    destruct (leqP t2 (t1 + F)) as [NEQ1|NEQ1]; last destruct (leqP F Δ) as [NEQ2|NEQ2].
+    { rewrite -leq_subLR in NEQ1.
+      rewrite -(leqRW NEQ1) (leqRW RTC) (leqRW (service_at_most_cost _ _ _ _ _)) //
+              (leqRW (service_within_busy_interval_ge_job_cost  _ _ _ _ _ _ _)) //.
+      rewrite (leqRW (cumulative_interference_sub _ _ t1 _ t1 t2 _ _)) //. 
+      have LLL : (t1 < t2) = true by apply leq_ltn_trans with (t1 + Δ); lia.
+      interval_to_duration t1 t2 k.
+      eapply leq_trans.
+      - by rewrite addnC; (eapply service_and_interference_bounded with (t := t1) (t3 := t1+k)
+                        || eapply service_and_interference_bounded with (t := t1) (t2 := t1+k)).
+      - lia.
+    }
+    { have NoInterference: cumulative_interference j (t1 + F) (t1 + Δ) = 0.
+      { rewrite /cumulative_interference /cumul_cond_interference big_nat.
+        apply big1; move => t /andP [GE__t LT__t].
+        apply/eqP; rewrite eqb0; apply/negP; eapply H_work_conserving => //.
+        { by apply/andP; split; lia. }
+        apply: H_ideal_progress_proc_model.
+        apply: job_nonpreemptive_after_run_to_completion_threshold GE__t _ _ => //.
+        - by rewrite -(leqRW RTC); apply H_valid_run_to_completion_threshold.
+        - by move: NCOM; apply contra; apply completion_monotonic; lia.
+      }
+      rewrite (leqRW RTC); erewrite cumulative_interference_cat with (t := t1 + F); last by lia.
+      rewrite /cumulative_interference in NoInterference.
+      rewrite NoInterference addn0; erewrite no_service_before_busy_interval => //.
+      by rewrite addnC; apply: service_and_interference_bounded.
+    }
+    { rewrite (leqRW RTC) (leqRW (cumulative_interference_sub _ _ t1 _ t1 (t1 + F) _ _ )); try lia.
+      erewrite no_service_before_busy_interval => //.
+      by rewrite addnC; eapply service_and_interference_bounded. }
+  Qed.
+
+  (** For simplicity, let's define a local name for the search space. *)
+  Let is_in_search_space A := is_in_search_space L interference_bound_function A.
+
+  (** Consider any value [R] that upper-bounds the solution of each
+      response-time recurrence, i.e., for any relative arrival time A
+      in the search space, there exists a corresponding solution [F]
+      such that [F + (task_cost tsk - task_rtc tsk) <= R]. *)
+  Variable R : duration.
+  Hypothesis H_R_is_maximum_ideal :
+    forall A,
+      is_in_search_space A ->
+      exists F,
+        task_rtct tsk + interference_bound_function A (A + F) <= A + F /\
+        F + (task_cost tsk - task_rtct tsk) <= R.
+
+  (** Using the lemma about [IBF_NP], we instantiate the general RTA
+      theorem's result to the ideal uniprocessor's case to prove that
+      [R] is a response-time bound. *)
+  Theorem uniprocessor_response_time_bound_ideal :
+    task_response_time_bound arr_seq sched tsk R.
+  Proof.
+    eapply uniprocessor_response_time_bound with (IBF_NP := fun F Δ => F - task_rtct tsk) => //.
+    { by apply nonpreemptive_interference_is_bounded. }
+    { move => F _.
+      destruct (leqP F (task_rtct tsk)) as [NEQ|NEQ].
+      - eapply leq_trans; [apply NEQ | ].
+        by eapply leq_trans; [apply H_valid_run_to_completion_threshold | lia].
+      - by rewrite addnBCA; [lia | apply H_valid_run_to_completion_threshold | lia].
+    }
+    { move => A SP; specialize (H_R_is_maximum_ideal A SP).
+      destruct H_R_is_maximum_ideal as [F [EQ1 EQ2]].
+      exists (A + F); split=> [//|].
+      eapply leq_trans; [ | by erewrite leq_add2l; apply EQ2].
+      by rewrite addnBCA; [lia | apply H_valid_run_to_completion_threshold | lia].
+    }
+  Qed.
+
+End AbstractRTAIdeal.

analysis/abstract/ideal/abstract_seq_rta.v

+Require Export prosa.analysis.definitions.task_schedule.
+Require Export prosa.analysis.facts.model.rbf.
+Require Export prosa.analysis.facts.model.task_arrivals.
+Require Export prosa.analysis.facts.model.task_schedule.
+Require Export prosa.analysis.facts.model.sequential.
+Require Export prosa.analysis.abstract.ideal.abstract_rta.
+Require Export prosa.analysis.abstract.IBF.task.
+
+(** * Abstract Response-Time Analysis with sequential tasks *)
+(** In this section we propose the general framework for response-time
+    analysis (RTA) of uni-processor scheduling of real-time tasks with
+    arbitrary arrival models and sequential tasks. *)
+
+(** We prove that the maximum among the solutions of the response-time
+    bound recurrence for some set of parameters is a response-time
+    bound for [tsk].  Note that in this section we _do_ rely on the
+    hypothesis about task sequentiality. This allows us to provide a
+    more precise response-time bound function, since jobs of the same
+    task will be executed strictly in the order they arrive. *)
+Section Sequential_Abstract_RTA.
+
+  (** Consider any type of tasks ... *)
+  Context {Task : TaskType}.
+  Context `{TaskCost Task}.
+  Context `{TaskRunToCompletionThreshold Task}.
+
+  (**  ... and any type of jobs associated with these tasks. *)
+  Context {Job : JobType}.
+  Context `{JobTask Job Task}.
+  Context `{JobArrival Job}.
+  Context `{JobCost Job}.
+  Context `{JobPreemptable Job}.
+
+  (** Consider any kind of ideal uni-processor state model. *)
+  Context `{PState : ProcessorState Job}.
+  Hypothesis H_uniprocessor_proc_model : uniprocessor_model PState.
+  Hypothesis H_unit_service_proc_model : unit_service_proc_model PState.
+  Hypothesis H_ideal_progress_proc_model : ideal_progress_proc_model PState.
+
+  (** Consider any valid arrival sequence with consistent, non-duplicate arrivals...*)
+  Variable arr_seq : arrival_sequence Job.
+  Hypothesis H_valid_arrival_sequence : valid_arrival_sequence arr_seq.
+
+  (** ... and any ideal schedule of this arrival sequence. *)
+  Variable sched : schedule PState.
+  Hypothesis H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched arr_seq.
+
+  (** ... where jobs do not execute before their arrival nor after completion. *)
+  Hypothesis H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched.
+  Hypothesis H_completed_jobs_dont_execute : completed_jobs_dont_execute sched.
+
+  (** Assume that the job costs are no larger than the task costs. *)
+  Hypothesis H_valid_job_cost : arrivals_have_valid_job_costs arr_seq.
+
+  (** Consider an arbitrary task set. *)
+  Variable ts : list Task.
+
+  (** Let [tsk] be any task in ts that is to be analyzed. *)
+  Variable tsk : Task.
+  Hypothesis H_tsk_in_ts : tsk \in ts.
+
+  (** Consider a valid preemption model ... *)
+  Hypothesis H_valid_preemption_model : valid_preemption_model arr_seq sched.
+
+  (** ...and a valid task run-to-completion threshold function. That
+      is, [task_rtct tsk] is (1) no bigger than [tsk]'s cost, (2) for
+      any job of task [tsk] [job_rtct] is bounded by [task_rtct]. *)
+  Hypothesis H_valid_run_to_completion_threshold :
+    valid_task_run_to_completion_threshold arr_seq tsk.
+
+  (** Let [max_arrivals] be a family of valid arrival curves, i.e.,
+      for any task [tsk] in [ts], [max_arrival tsk] is (1) an arrival
+      bound of [tsk], and (2) it is a monotonic function that equals
+      [0] for the empty interval [delta = 0]. *)
+  Context `{MaxArrivals Task}.
+  Hypothesis H_valid_arrival_curve : valid_taskset_arrival_curve ts max_arrivals.
+  Hypothesis H_is_arrival_curve : taskset_respects_max_arrivals arr_seq ts.
+
+  (** Assume we are provided with abstract functions for interference
+      and interfering workload. *)
+  Context `{Interference Job}.
+  Context `{InterferingWorkload Job}.
+
+  (** We assume that the schedule is work-conserving. *)
+  Hypothesis H_work_conserving : work_conserving arr_seq sched.
+
+  (** Unlike the previous theorem
+      [uniprocessor_response_time_bound_ideal], we assume that (1)
+      tasks are sequential, moreover (2) functions interference and
+      interfering_workload are consistent with the hypothesis of
+      sequential tasks. *)
+  Hypothesis H_sequential_tasks : sequential_tasks arr_seq sched.
+  Hypothesis H_interference_and_workload_consistent_with_sequential_tasks :
+    interference_and_workload_consistent_with_sequential_tasks arr_seq sched tsk.
+
+  (** Assume we have a constant [L] that bounds the busy interval of
+      any of [tsk]'s jobs. *)
+  Variable L : duration.
+  Hypothesis H_busy_interval_exists :
+    busy_intervals_are_bounded_by arr_seq sched tsk L.
+
+  (** Next, we assume that [task_IBF] is a bound on interference
+      incurred by the task. *)
+  Variable task_IBF : duration -> duration -> duration.
+  Hypothesis H_task_interference_is_bounded :
+    task_interference_is_bounded_by arr_seq sched tsk task_IBF.
+
+  (** Let us abbreviate task [tsk]'s RBF for clarity. *)
+  Let task_rbf := task_request_bound_function tsk.
+
+  (** Given any job [j] of task [tsk] that arrives exactly [A] units
+      after the beginning of the busy interval, the bound on the total
+      interference incurred by [j] within an interval of length [Δ] is
+      no greater than [task_rbf (A + ε) - task_cost tsk + task's IBF
+      Δ]. Note that in case of sequential tasks the bound consists of
+      two parts: (1) the part that bounds the interference received
+      from other jobs of task [tsk] -- [task_rbf (A + ε) - task_cost
+      tsk] and (2) any other interference that is bounded by
+      [task_IBF(tsk, A, Δ)]. *)
+  Let total_interference_bound (A Δ : duration) :=
+    task_rbf (A + ε) - task_cost tsk + task_IBF A Δ.
+
+  (** Note that since we consider the modified interference bound
+      function, the search space has also changed. One can see that
+      the new search space is guaranteed to include any A for which
+      [task_rbf (A) ≠ task_rbf (A + ε)], since this implies the fact
+      that [total_interference_bound (A, Δ) ≠ total_interference_bound
+      (A + ε, Δ)]. *)
+  Let is_in_search_space_seq := is_in_search_space L total_interference_bound.
+
+  (** Consider any value [R], and assume that for any relative arrival
+      time [A] from the search space there is a solution [F] of the
+      response-time recurrence that is bounded by [R]. In contrast to
+      the formula in "non-sequential" Abstract RTA, assuming that
+      tasks are sequential leads to a more precise response-time
+      bound. Now we can explicitly express the interference caused by
+      other jobs of the task under consideration.
+
+      To understand the right part of the fix-point in the equation,
+      it is helpful to note that the bound on the total interference
+      ([bound_of_total_interference]) is equal to [task_rbf (A + ε) -
+      task_cost tsk + task_IBF tsk A Δ]. Besides, a job must receive
+      enough service to become non-preemptive [task_lock_in_service
+      tsk]. The sum of these two quantities is exactly the right-hand
+      side of the equation. *)
+  Variable R : duration.
+  Hypothesis H_R_is_maximum_seq :
+    forall (A : duration),
+      is_in_search_space_seq A ->
+      exists (F : duration),
+        A + F >= (task_rbf (A + ε) - (task_cost tsk - task_rtct tsk)) + task_IBF A (A + F)
+        /\ R >= F + (task_cost tsk - task_rtct tsk).
+
+  (** Since we are going to use the
+      [uniprocessor_response_time_bound_ideal] theorem to prove the
+      theorem of this section, we have to show that all the hypotheses
+      are satisfied. Namely, we need to show that [H_R_is_maximum_seq]
+      implies [H_R_is_maximum]. Note that the fact that hypotheses
+      [H_sequential_tasks, H_i_w_are_task_consistent and
+      H_task_interference_is_bounded_by] imply
+      [H_job_interference_is_bounded] is proven in the file
+      [analysis/abstract/IBF/task]. *)
+
+  (** In this section, we prove that [H_R_is_maximum_seq] implies [H_R_is_maximum]. *)
+  Section MaxInSeqHypothesisImpMaxInNonseqHypothesis.
+
+    (** To rule out pathological cases with the [H_R_is_maximum_seq]
+        equation (such as [task_cost tsk] being greater than [task_rbf
+        (A + ε)]), we assume that the arrival curve is
+        non-pathological. *)
+    Hypothesis H_arrival_curve_pos : 0 < max_arrivals tsk ε.
+
+    (** For simplicity, let's define a local name for the search space. *)
+    Let is_in_search_space A :=
+      is_in_search_space L total_interference_bound A.
+
+    (** We prove that [H_R_is_maximum] holds. *)
+    Lemma max_in_seq_hypothesis_implies_max_in_nonseq_hypothesis:
+      forall (A : duration),
+        is_in_search_space A ->
+        exists (F : duration),
+          A + F >= task_rtct tsk +
+                    (task_rbf (A + ε) - task_cost tsk + task_IBF A (A + F))
+          /\ R >= F + (task_cost tsk - task_rtct tsk).
+    Proof.
+      move: H_valid_run_to_completion_threshold => [PRT1 PRT2]; move => A INSP.
+      clear H_sequential_tasks H_interference_and_workload_consistent_with_sequential_tasks.
+      move: (H_R_is_maximum_seq _ INSP) => [F [FIX LE]].
+      exists F; split=> [|//].
+      rewrite -{2}(leqRW FIX).
+      rewrite addnA leq_add2r.
+      rewrite addnBA; last first.
+      { apply leq_trans with (task_rbf 1).
+        - exact: task_rbf_1_ge_task_cost.
+        - by apply: task_rbf_monotone => //; rewrite addn1.
+      }
+      by rewrite subnBA; auto; rewrite addnC.
+    Qed.
+
+  End MaxInSeqHypothesisImpMaxInNonseqHypothesis.
+
+  (** We apply the [uniprocessor_response_time_bound_ideal] theorem,
+      and using the lemmas proven earlier, we prove that all the
+      requirements are satisfied. So, [R] is a response-time bound. *)
+  Theorem uniprocessor_response_time_bound_seq :
+    task_response_time_bound arr_seq sched tsk R.
+  Proof.
+    move => j ARR TSK.
+    eapply uniprocessor_response_time_bound_ideal => //.
+    { exact: task_IBF_implies_job_IBF => //. }
+    { exact: max_in_seq_hypothesis_implies_max_in_nonseq_hypothesis => //. }
+  Qed.
+
+End Sequential_Abstract_RTA.

analysis/abstract/ideal/cumulative_bounds.v

+Require Export analysis.abstract.ideal.iw_instantiation.
+
+(** In this file, we prove some inequalities that always
+    hold inside the busy interval of a job. Throughout this file we
+    assume the ideal uniprocessor model. *)
+Section BusyIntervalInequalities.
+
+  (** Consider any kind of tasks and their jobs, each characterized by
+      an arrival time, a cost, and an arbitrary notion of readiness. *)
+  Context {Task : TaskType} {Job : JobType} `{JobTask Job Task}.
+  Context `{JobArrival Job} `{JobCost Job} {JR :JobReady Job (ideal.processor_state Job)}.
+
+  (** Consider a JLFP policy that is reflexive and respects sequential tasks. *)
+  Context {JLFP : JLFP_policy Job}.
+  Hypothesis H_policy_is_reflexive : reflexive_job_priorities JLFP.
+  Hypothesis H_policy_respecsts_sequential_tasks : policy_respects_sequential_tasks JLFP.
+
+  (** Consider a consistent arrival sequence that does not contain duplicates. *)
+  Variable arr_seq : arrival_sequence Job.
+  Hypothesis H_valid_arrival_sequence : valid_arrival_sequence arr_seq.
+
+  (** Consider any valid ideal uniprocessor schedule defined over this arrival sequence. *)
+  Variable sched : schedule (ideal.processor_state Job).
+  Hypothesis H_valid_schedule : valid_schedule sched  arr_seq.
+
+  (** Consider a set of tasks [ts] that contains all the jobs in the
+      arrival sequence. *)
+  Variable ts : list Task.
+  Hypothesis H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts.
+
+  (** Consider a task [tsk]. *)
+  Variable tsk : Task.
+
+  (** Consider a job [j] of the task [tsk] that has a positive job cost. *)
+  Variable j : Job.
+  Hypothesis H_j_arrives : arrives_in arr_seq j.
+  Hypothesis H_job_of_tsk : job_of_task tsk j.
+  Hypothesis H_job_cost_positive: job_cost_positive j.
+
+  (** Consider the ideal JLFP definitions of interference and
+      interfering workload. *)
+  #[local] Instance ideal_jlfp_interference : Interference Job :=
+    ideal_jlfp_interference arr_seq sched.
+
+  #[local] Instance ideal_jlfp_interfering_workload : InterferingWorkload Job :=
+    ideal_jlfp_interfering_workload arr_seq sched.
+
+  (** Consider the busy interval for j is given by <<[t1,t2)>>. *)
+  Variable t1 t2 : duration.
+  Hypothesis H_busy_interval : definitions.busy_interval sched j t1 t2.
+
+  (** Let us denote the relative arrival time by [A]. *)
+  Let A := job_arrival j - t1.
+
+  (** Consider any arbitrary time [Δ] inside the busy interval. *)
+  Variable  Δ : duration.
+  Hypothesis H_Δ_in_busy : t1 + Δ <= t2.
+
+  (** First, we prove that if the priority inversion is bounded then,
+      the cumulative priority inversion is also bounded. *)
+  Section PIBound.
+
+    (** Consider the priority inversion in any given interval
+        is bounded by a constant. *)
+    Variable priority_inversion_bound : duration -> duration.
+    Hypothesis H_priority_inversion_is_bounded :
+      priority_inversion_is_bounded_by arr_seq sched tsk priority_inversion_bound.
+
+    (** Then, the cumulative priority inversion in any interval
+        is also bounded. *)
+    Lemma cumulative_priority_inversion_is_bounded:
+      cumulative_priority_inversion arr_seq sched j t1 (t1 + Δ)
+      <= priority_inversion_bound (job_arrival j - t1).
+    Proof.
+      apply leq_trans with (cumulative_priority_inversion arr_seq sched j t1 t2).
+      - rewrite [X in _ <= X](@big_cat_nat _ _ _ (t1  + Δ)) //=; try by lia.
+        by rewrite /priority_inversion leq_addr.
+      - apply: H_priority_inversion_is_bounded => //.
+        by move: H_busy_interval; rewrite -instantiated_busy_interval_equivalent_busy_interval // =>  -[PREF _].
+    Qed.
+
+  End PIBound.
+
+  (** Let [jobs] denote the arrivals in the interval [Δ]. *)
+  Let jobs := arrivals_between arr_seq t1 (t1 + Δ).
+
+  (** Next, we prove that the cumulative interference from higher priority
+      jobs of other tasks in an interval is bounded by the total service
+      received by the higher priority jobs of those tasks. *)
+  Lemma cumulative_interference_is_bounded_by_total_service:
+    cumulative_another_task_hep_job_interference arr_seq sched j t1 (t1 + Δ)
+    <= service_of_jobs sched (fun jo => another_task_hep_job jo j) jobs t1 (t1 + Δ).
+  Proof.
+    move: (H_busy_interval) => [[/andP [JINBI JINBI2] [QT _]] _].
+    rewrite cumulative_i_thep_eq_service_of_othep => //.
+    have /eqP TSK := H_job_of_tsk.
+    by rewrite instantiated_quiet_time_equivalent_quiet_time.
+  Qed.
+
+End BusyIntervalInequalities.