Getting started with Prosa

Prosa Foundations

The Prosa framework is built on top of the Coq proof assistant and the ssreflect extension from the Mathematical Components library.

Coq is a proof assistant based on a higher-order logic with support for computation. That is, apart from writing specifications and proving theorems, in Coq it is also possible to write programs (as recursive functions) and prove claims about them.

Prosa uses the computational capabilities of Coq to implement schedulability analyses, and then states and proves schedulability claims about the implemented analyses (e.g., of the form “if this algorithm returns ‘no deadline missed’, then there does not exist a schedule matching the stated assumptions in which a deadline is missed”).

Ssreflect, in turn, is an extension for Coq that originated in the development of the formal proof of the Four Color Theorem. Apart from several improvements in the proof tactics, ssreflect includes many libraries for mathematical reasoning. One of these libraries, bigop, is used pervasively throughout Prosa to declare LaTeX-like operators such as \sum.

To install Coq and ssreflect on your computer, check out the setup instructions.

Reading the Specification vs. Writing Proofs

There are three basic ways of working with Prosa, each of which requires different levels of expertise in Coq.

  1. Specification Reader (1 hour crash course in Coq): By reading the specification, one can check whether Prosa’s formalization of real-time scheduling concepts matches the view informally agreed upon by the real-time community or the specific assumptions in a particular paper. This is a crucial role — the trust in the formal proofs derives from the fact that the specification is read, and deemed to be reasonable, by as many experts as possible. Prosa’s goals and principles are intended to make this task as easy as possible.

    Anyone with a background in real-time scheduling and informal logic should be able to quickly pick up the essential syntax needed to read the specification in a matter of roughly an hour. To get started, read the essential syntax primer below.

  2. Specification Writer (basic experience in Coq): The specification writer is responsible for writing and critiquing definitions, theorem statements, and commentary, all of which compose the “external view” of Prosa that is intended to be read and checked by specification readers. Another important task that specification writers help with is to organize and subdivide the overall proof outline into (many) simple, intermediate lemmas (i.e., to help break the proof into small steps), to clearly expose the high-level strategy and the underlying intuition of the proof to readers.

    Someone who is already comfortable with functional programming and precise mathematical specifications can acquire the minimal Coq background needed to get started as a specification writer in a few days. Obviously more time is required for someone coming from a more distant background.

  3. Proof Writer (extensive experience in Coq): The proof writer is responsible for proving the theorems and lemmas, and for guiding the specification writers. Since misconceptions about the model (e.g., insufficient or mismatching assumptions) tend to become apparent only when writing proof scripts, there must be a constant feedback cycle and collaboration between proof writers and specification writers.

    Writing proof scripts is not trivial and requires some familiarity with Coq and ssreflect, which takes a couple of months to become fluent (see proof prerequisites).

Based on our experience with Prosa, this division naturally maps to a workflow in which co-authors of various levels of Coq expertise collaborate to develop formal proofs, as illustrated in the figure below.

Figure: Prosa Workflow
Figure: Prosa Workflow

Essential Syntax Primer

In the following, we provide a short guide for reading specifications in Prosa.

Note: this primer is still a work in progress; feedback, improvements, and corrections are very welcome.

1. Stating Assumptions

Assumptions in Coq can be stated with the keyword Hypothesis. For example, this is how we assume that tasks have constrained deadlines.

  (* Assume that tasks have constrained deadlines. *)
  Hypothesis H_constrained_deadlines:
       tsk, tsk ts task_deadline tsk task_period tsk.

Prosa makes extensive use of Coq’s Hypothesis feature to make all assumptions explicit.

2. Stating Definitions

In Coq, a Definition creates an alias to an expression. For example, the following statement defines a pending job as a job that has arrived but has not yet completed.

  (* Job j is pending at time t iff it has arrived but has not completed. *)
  Definition pending (t: time) := has_arrived j t ¬ completed t.

Here, the name pending is bound to a function with a parameter t of type time.

Prosa uses definitions extensively to define simple predicates, which usually are defined in terms of simpler predicates. For example, pending is defined in terms of the more basic notions of has_arrived j t (the job #j# is released on or prior to time #t#) and ¬ completed t (the job #j# is not yet complete at time #t#).

3. Lemmas and Theorems

In Coq, lemmas, theorems, corollaries, remarks, and facts are all the same thing: aliases to proof terms. A Lemma, for example, can be declared as follows. (For simplicity, some variables from the context are omitted.)

  (* The service received by any job j at any time t is at most 1. *)
  Lemma service_at_most_one :
     t, service_at sched j t 1.
  Proof.
    (omitted...)
  Qed.

Note that Coq only allows a lemma to be declared if a correct proof is provided.

5. Sections Delimit the Specification

In Coq, a Section creates a scope wherein variables can be instantiated and/or constrained.

Section Completion.

    (* Assume that completed jobs do not execute. *)
     Hypothesis H_completed_jobs:
      completed_jobs_dont_execute job_cost sched.

    (* Let j be any job in the arrival sequence. *)
    Variable j: JobIn arr_seq.

    (* If job j has completed, then it cannot be scheduled. *)
    Lemma completed_implies_not_scheduled :
       t,
        completed job_cost sched j t
        ¬ scheduled sched j t.

End Completion.

The variables introduced in a section are defined only within the scope of the section. By default, variables are entirely unrestricted: every variable is universally quantified, i.e., there is an implied “for all possible values”.

Generality can be restricted within a section by explicitly stating assumptions. For example, in the shown segment, the claim is restricted to apply only to schedules (any sched) in which jobs cease to execute after having received an amount of processor service equal to their execution cost (as determined by job_cost).

Any definition or lemma stated within the section can be accessed from outside, under two conditions:

  1. when reusing definitions and lemmas, any variable declared in the section must be passed explicitly, and

  2. when reusing lemmas only, any stated hypothesis must be supplied (i.e., proven to hold in the external context).

In the example above, this means that we can only use the proven lemma outside this section if we supply both a proof of the hypothesis that “completed jobs do not execute” and some job #j# to be considered.

Finally, note that Coq keeps track of the dependencies across definitions and lemmas. Therefore, there is no need to supply hypotheses that are not used by the lemmas we want to access, even if such hypotheses are redundantly assumed in the corresponding section.

6. LaTeX-like Operators

The library bigops from ssreflect allows defining arbitrary functions based on summation (#\sum#), product (#\prod#), and any other customized operator. This provides a natural and clear notation for definitions that might otherwise require ad hoc recursion.

One example of the use of bigop is our definition of instantaneous service of a job, which just counts the number of processors where a job is scheduled.

  (* The instantaneous service of job j at time t is the number of cpus where it is scheduled on.
    Note that we use a sum to account for parallelism if required. *)

  Definition service_at (t: time) :=
    \sum_(cpu < num_cpus | scheduled_on cpu t) 1.

The rest of this guide is concerned with developing new proofs.

Proof Prerequisites: Coq and Ssreflect

To develop proofs in Prosa, there are two prerequisites. First, one must know how to prove theorems in Coq (i.e., apply lemmas, perform case analysis, use induction, etc.). After that, one should learn the basics of ssreflect (tactics, boolean reflection and the libraries used by Prosa). To help with this process, we recommend some study material for learning Coq and ssreflect.

1. Learning Coq

For a gentle Coq tutorial, we recommend the first couple of chapters of the Software Foundations book by Pierce et al., available for free on their webpage. The final chapters of the book (starting from Imp: Simple Imperative Programs) cover programming languages semantics and can be safely ignored (in the context of Prosa).

Alternatively, one can also read the Mathematical Components book, which introduces Coq in the context of the Mathematical Components library, thus with the same syntax used by Prosa.

Other sources for documentation and guides are listed on the Coq webpage.

2. Learning Ssreflect

Ssreflect can be learned in two steps: (1) getting used to the new tactics and notation, and (2) learning the new mathematical theories (definitions and lemmas).

For an introduction to the new tactics, please refer to the Mathematical Components book and the Ssreflect manual. Moreover, some examples are also given in the tutorial that was held at the Advanced Coq Winter School.

To learn the new theories, note that the core of Prosa uses only six of the basic ssreflect libraries:

This limited scope makes it possible to learn Prosa by studying and emulating the existing proofs while ignoring the more complex parts of Mathematical Components; to this end, reading the coqdoc documentation of the existing Prosa proofs is helpful. For additional material, please check the Mathematical Components book and the tutorials from ITP13 (see also the video) and the Advanced Coq Winter School.

Even after learning how to use the libraries, carrying out mechanized proofs requires some practice, so please feel free to send questions to our mailing list in case of problems.