guidelines.md 10.2 KB
Newer Older
1 2
# Writing and Coding Guidelines

3
This project targets Coq *non*-experts. Accordingly, great emphasis is placed on keeping it as simple and as accessible as possible.
4

5 6
## Core Principles

7 8 9
1. **Readability** matters most. Specifications that are difficult to grasp are fundamentally no more trustworthy than pen&paper proofs.
2. Being **explicit** is good. The overarching goal is to make it easy for the (non-expert) reader. Being explicit and (within reason) verbose and at times repetitive helps to make a spec more readable because most statements can then be understood within a local scope. Conversely, any advanced "magic" that works behind the scenes can quickly render a spec unreadable to novices.
3. **Good names** are essential. Choose long, self-explanatory names. Even if this means "more work" when typing the name a lot, it greatly helps with providing a helpful intuition to the reader. (Note to advanced users: if you find the long names annoying, consider using [Company Coq](https://github.com/cpitclaudel/company-coq)'s autocompletion features.)
10
4. **Comment** profusely. Make an effort to comment all high-level steps and definitions. In particular, comment all hypotheses, definitions, lemmas, etc.
11
5. **Keep it simple.** Shy away from advanced Coq techniques. At the very least, the spec and all lemma/theorem claims should be readable and understandable with a basic understanding of Coq (proofs are not expected to be readable).
12 13


14
## Readability Advice
15 16

- Use many, mostly short sections. Sections are a great way to structure code and to guide the reader; they serve the reader by establishing a local scope that is easier to remember.
17 18
- Keep definitions and proofs in separate sections, and ideally in different files. This makes the definitions short, and more clearly separates the computation of the actual analysis results from their validity arguments.
- Make extensive use of the `Hypothesis` feature. Hypotheses are very readable and are accessible even to non-Coq users, especially when paired with self-explanatory names.
19
- Consider renaming general concepts with `let` bindings to introduce local names that are more meaningful. In many cases, this is also useful to bind necessary context to local names. For example:  
20
```
21 22
    Let no_deadline_is_missed :=
      task_misses_no_deadline sched tsk.
23
``` 
24
- Interleave running commentary *as if you were writing a paper* with the actual definitions and lemmas. This helps greatly with making the spec more accessible to everyone. Good example from [bertogna_fp_theory.v](../classic/analysis/global/basic/bertogna_fp_theory.v):  
25
```
26
   (** Assume any job arrival sequence... *)
27
    Context {arr_seq: arrival_sequence Job}.
28
   (** ... in which jobs arrive sporadically and have valid parameters. *)
29 30 31
    Hypothesis H_sporadic_tasks:
      sporadic_task_model task_period arr_seq job_task.
```
Marco Maida's avatar
Marco Maida committed
32 33 34
- When commenting, be careful not to leave any misspelled words: Prosa's CI system comprises a spell-checker that will signal errors.
- When comments have to contain variable names or mathematical notation, use square brackets (e.g. `[job_cost j]`). You can nest square brackets _only if they are balanced_: `[[t1,t2)]` will not work. In this case, use `<<[t1,t2)>>`.
- The vocabulary of the spell-checker is extended with the words contained in `scripts/wordlist.pws`. Add new words only if strictly necessary.
35 36 37
- Document the sources of lemmas and theorems in the comments. For example, say something like "Theorem XXX in (Foo & Bar, 2007)", and document at the beginning of the file what "(Foo & Bar, 2007)" refers to.


38 39 40
## Naming Conventions

1. For consistency, start the name of hypotheses with `H_`.
41 42 43
2. For case a case analysis of `foo`, use `foo_cases` as the lemma name.
3. For a basic lemma that is intended as a rewriting rule to avoid unfolding a definition `foo` directly, use `foo_def` as the lemma name.
4. Consistently name predicates that express that something "is valid" (i.e., satisfies basic assumptions) as `valid_*` or `respects_*`.  
44
Examples: `valid_schedule`, `taskset_respects_sporadic_task_model`. 
45
5. Consistently name sections that define what it means to be valid w.r.t. to some concept `Foo` as `ValidFoo`.  
46
Examples: `ValidSchedule`,  `ValidTask`, `ValidJobOfTask`, `ValidJobsOfTask`.
47
6. Job parameters are always prefixed with `job_`.  
48
Examples: `job_cost`, `job_arrival`, `job_deadline`. 
49 50 51
7. Task parameters are always prefixed with `task_`.  
Examples: `task_cost`, `task_deadline`.
8. We do not follow ssreflect's concise but not so self-explanatory naming scheme. 
52 53 54 55


## Coq Features

56
- We use type classes sparingly. Primarily, type classes are used to introduce new job and task parameters, and to express key modeling assumptions (e.g., whether jobs can self-suspend or not).
57 58 59 60
- We rely heavily on type inference. Top-level definitions do *not* require type annotations if the semantics are clear from context and Coq can figure out the specific types.
- We tend to not use a lot of custom syntax/notation. Heavy use of custom syntax reduces readability because readers are forced to remember all local syntax definitions. 
- We rely heavily on ssreflect notation.

61 62 63 64 65 66 67 68
## Structuring Specifications

1. Split specifications into succinct, logically self-contained files/modules. As a rule of thumb, use one file/module per concept.
2. As stated above, use `Section`s liberally within each file. However, avoid needless sections, i.e., a section without a single variable, context declaration, or hypothesis serves no purpose and can/should be removed. 
3. Prefer `Require Export full.path.to.module.that.you.want` over `From full.path.to.module.that.you Require Export want` because (as of Coq 8.10) the latter is brittle w.r.t. Coq's auto-magic module finding heuristics (see also: Coq issues [9080](https://github.com/coq/coq/issues/9080), [9839](https://github.com/coq/coq/issues/9839), and [11124](https://github.com/coq/coq/issues/11124)).  
Exception to this rule: ssreflect and other standard library imports. 
4. Avoid repetitive, lengthy blocks of `Require Import` statements at the beginning of files through the judicious use of `Require Export`.
5. As an import exception to the prior rule, *never* re-export modules that contain type class instance definitions. Prosa uses type class instances to express key modeling choices; such assumptions need to be made explicit and should not be implicitly "inherited" via re-exported modules. 
69

70 71
## Writing Proofs

72 73 74 75 76
When writing new proofs, please adhere to the following rules.

### Structure

1. Keep proofs short. Aim for just a few lines, and definitely not more than 30-40. Long arguments should be structured into many individual lemmas (in their own section) that correspond to high-level proof steps. Some exceptions may be needed, but such cases should truly remain *exceptional*.  
77
Note: We employ an automatic proof-length checker that runs as part of continuous integration to enforce this.
78 79 80
2. However, making proofs as concise as possible is a *non-goal*. We are **not** playing [code golf](https://en.wikipedia.org/wiki/Code_golf). If a proof is too long, the right answer is usually **not** to maximally compress it; rather, one should identify semantically meaningful steps that can be factored out and documented as local  "helper" lemmas. Many small steps are good for readability.
3. Make use of the structured sub-proofs feature (i.e., indentation with `{` and `}`, or bulleted sub-proofs with `-`, `+`, `*`) to structure code.
4. Make proofs "step-able." This means preferring `.` over `;` (within reason). This makes it easier for novices to learn from existing proofs.
81

82

83
### Maintainability
84

85
Generally try to make proofs as robust to (minor) changes in definitions as possible. Longterm maintenance is a major concern.
86

87
1. Make use of the `by` tactical to stop the proof script early in case of any changes in assumptions.
88
2. General principle: **Rewrite with equalities, do not unfold definitions.**   
89
Avoid unfolding definitions in anything but “basic facts” files. Main proofs should not unfold low-level definitions, processor models, etc. Rather, they should rely exclusively on basic facts so that we can change representations without breaking high-level proofs.
Björn Brandenburg's avatar
Björn Brandenburg committed
90 91
3. In particular, for case analysis, prefer basic facts that express all possible cases as a disjunction. Do not destruct the actual definitions directly.
    - Aside: Sometimes, it is more convenient to use a specific inductive type rather than a disjunction. See for instance `PeanoNat.Nat.compare_spec` in the Coq standard library or Section 4.2.1 of the [Mathcomp book](https://math-comp.github.io/mcb/book.pdf) for more details. However, we generally prefer disjunctions for readability whenever possible and reasonable. 
92
4. Do not explicitly reference proof terms in type classes (because they might change with the representation). Instead, introduce lemmas that restate the proof term in a general, abstract way that is unlikely to change and rely on those.  
93
Guideline: do not name proof terms in type classes to prevent explicit dependencies.
94

95
### Tactics
96

Björn Brandenburg's avatar
Björn Brandenburg committed
97
- Document the tactics that you use in the [list of tactics](doc/tactics.md). For new users, it can be quite difficult to identify the right tactics to use. This list is intended to give novices a starting to point in the search for the "right" tools.
98

99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135
### Forward vs backward reasoning
Although the primary focus of Prosa is on the quality of the overall structure and the specifications, good proofs are short and readable. Since Coq tends to favor backward reasoning, try to adhere to it. Forward reasoning tends to be more verbose and to generate needlessly convoluted proof trees. To get an idea, read the following snippet:
```
(* Let's say A->B->C->D *)
  Variable A B C D : Prop.
  Hypothesis AB : A->B.
  Hypothesis BC : B->C.
  Hypothesis CD : C->D.

  (* And we want to prove A->D *)
  Lemma AD_backward:
    A->D.
  Proof.
    intros.
    apply CD.
    apply BC.
    now apply AB.
  Qed.

  Lemma AD_forward:
    A->D.
  Proof.
    intros.
    (* hmm, I have C->D. If only I had C... *) 
    have I_need_C: C.
    { (* hmm, I have B->C. If only I had B... *)
      have I_need_B: B by apply AB.
      feed BC.
      apply I_need_B.
      now apply BC.
    }
    feed CD.
    apply I_need_C.
    now apply CD.
  Qed.
  ```

136

Björn Brandenburg's avatar
Björn Brandenburg committed
137
*To be continued… Merge requests welcome: please feel free to propose new advice and better guidelines.*
138