style_guide.md 3.36 KB
Newer Older
1 2 3 4
# Iris Style Guide

This document lays down syntactic conventions about how we usually write our
Iris proofs in Coq.  It is a work-in-progress.  This complements the tactic
Tej Chajed's avatar
Tej Chajed committed
5 6
documentation for the [proof mode](./proof_mode.md) and [HeapLang](./heap_lang.md) as
well as the [proof guide](.doco/proof_guide.md).
7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38

## Implicit generalization

We often use the implicit generalization feature of Coq, triggered by a backtic:
`` `{!term A B}`` means that an implicit argument of type `term A B` is added,
and if any of the identifiers that are used here is not yet bound, it gets added
as well.  Usually, `term` will be some existing type class or similar, and we
use this syntax to also generalize over `A` and `B`; then the above is
equivalent to `{A B} {Hterm: term A B}`.  The `!` in front of the term disables
an even stronger form of generalization, where if `term` is a type class then
all missing arguments get implicitly generalized as well.  This is sometimes
useful, e.g. we can write `` `{Countable C}`` instead of `` `{!EqDecision C,
!Countable C}``.  However, generally it is more important to be aware of the
assumptions you are making, so implicit generalization without `!` should be
avoided.

## Type class resolution control

When you are writing a module that exports some Iris term for others to use
(e.g., `join_handle` in the [spawn module](theories/heap_lang/lib/spawn.v)), be
sure to mark these terms as opaque for type class search at the *end* of your
module (and outside any section):
```
Typeclasses Opaque join_handle.
```
This makes sure that the proof mode does not "look into" your definition when it
is used by clients.

## Naming conventions for variables/arguments/hypotheses

### small letters

Robbert Krebbers's avatar
Robbert Krebbers committed
39 40
* a : A = cmraT or ofeT
* b : B = cmraT or ofeT
41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69
* c
* d
* e : expr = expressions
* f = some generic function
* g = some generic function
* h : heap
* i
* j
* k
* l
* m : iGst = ghost state
* m* = prefix for option
* n
* o
* p
* q
* r : iRes = resources
* s = state (STSs)
* s = stuckness bits
* t
* u
* v : val = values of language
* w
* x
* y
* z 

### capital letters

Robbert Krebbers's avatar
Robbert Krebbers committed
70 71
* A : Type, cmraT or ofeT
* B : Type, cmraT or ofeT
72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112
* C
* D   
* E : coPset = Viewshift masks
* F = a functor
* G
* H = hypotheses
* I = indexing sets
* J
* K : ectx = evaluation contexts
* K = keys of a map
* L
* M = maps / global CMRA
* N : namespace
* O 
* P : uPred, iProp or Prop
* Q : uPred, iProp or Prop
* R : uPred, iProp or Prop
* S : set state = state sets in STSs
* T : set token = token sets in STSs
* U
* V : abstraction of value type in frame shift assertions
* W
* X : sets
* Y : sets
* Z : sets

### small greek letters

* γ : gname
* σ : state = state of language
* φ : interpretation of STS/Auth

### capital greek letters

* Φ : general predicate (over uPred, iProp or Prop)
* Ψ : general predicate (over uPred, iProp or Prop)

## Naming conventions for algebraic classes

### Suffixes

Robbert Krebbers's avatar
Robbert Krebbers committed
113
* O: OFEs
114 115
* R: cameras
* UR: unital cameras or resources algebras
Robbert Krebbers's avatar
Robbert Krebbers committed
116
* F: functors (can be combined with all of the above, e.g. OF is an OFE functor)
Tej Chajed's avatar
Tej Chajed committed
117
* G: global camera functor management (typeclass; see [proof\_guide.md](./proof_guide.md))
118 119
* I: bunched implication logic (of type `bi`)
* SI: step-indexed bunched implication logic (of type `sbi`)
Paolo G. Giarrusso's avatar
Paolo G. Giarrusso committed
120
* T: canonical structures for algebraic classes (for example ofeT for OFEs, cmraT for cameras)
Tej Chajed's avatar
Tej Chajed committed
121
* Σ: global camera functor management (`gFunctors`; see [proof\_guide.md](./proof_guide.md))