Prosa v0.5 is the first release of Prosa to support POET.

Download the release here: prosa_v05.zip

The directory and module structure is organized as follows. First, the main parts, of which there are currently five (plus the classic Prosa version).

**prosa.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.**prosa.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.**prosa.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.**prosa.results**: The`results`

namespace contains all**high-level analysis results**.**prosa.implementation**: Concrete implementations of some of the axiomatic models to which the results apply.**prosa.implementation.refinements**: The refinements needed by POET to compute with large numbers, based on CoqEAL.**classic**: This module contains the “classic” version of Prosa as first presented at ECRTS’16.

All results published prior to 2020 build on this “classic” version of Prosa.

The v0.5 release of Prosa uses CoqdocJS to obtain a prettier spec.

- Read the Prosa v0.5 specification and proofs.

Alternatively, there is also a plain `coqdoc`

version without proofs (which is better suited for printing to PDF).

- Read the Prosa v0.5 specification without proofs.

We also provide HTML renderings of the **classic** (i.e., pre-2020) Prosa spec, which is no longer being developed:

- Recommended: CoqdocJS-prettified (with proofs)
- Alternative: plain coqdoc (without proofs):

Prosa can be installed using the OPAM package manager (>= 2.0).

```
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
```

`opam`

OPAM can also be used to install a local checkout. For example, this is done in the CI setup (see `.gitlab-ci.yaml`

).

```
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
```

Besides on Coq itself, Prosa depends on

- the
`ssreflect`

library of the Mathematical Components project, - the Micromega support for the Mathematical Components library provided by
`mczify`

, and - the The Coq Effective Algebra Library (optional, needed only for POET-related refinements).

These dependencies can be easily installed with OPAM.

```
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.

Assuming all dependencies are available (either via OPAM or compiled from source), compiling Prosa consists of only two steps.

First, create an appropriate `Makefile`

.

```
./create_makefile.sh
```

Alternatively, to avoid compiling the older “classic” Prosa, specify the `--without-classic`

option. This can speed up compilation considerably and is a good idea during development. (It’s also possible to *only* compile the “classic” Prosa by specifying the `--only-classic`

option, but this is rarely needed.)

```
./create_makefile.sh --without-classic
```

To avoid compiling the POET-related refinements (which require CoqEAL to be installed and inject a dependency on the *proof irrelevance* axiom), specify the switch `--without-refinements`

. For example, to skip both “classic” Prosa and the refinements library, use the following command:

```
./create_makefile.sh --without-classic --without-refinements
```

Second, compile the library.

```
make -j
```

Depending on how powerful your machine is, this will take a few minutes.

To check the correctness of all proofs, compile the code as described above and run `make validate`

.

```
make validate
```

You should see the following output, confirming that all proofs in Prosa were mechanically checked and do not include any additional `Axioms`

.

```
CONTEXT SUMMARY
===============
*Theory: Set is predicative
*Axioms:
Coq.Logic.ProofIrrelevance.proof_irrelevance
*Constants/Inductives relying on type-in-type: <none>
*Constants/Inductives relying on unsafe (co)fixpoints: <none>
*Inductives whose positivity is assumed: <none>
```

The assumption of proof irrelevance is introduced by the `CoqEAL`

library and can be avoided by running `./create_makefile.sh`

with the `--without-refinements`

flag.