1
2
3
4
5
6
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
39
40
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
70
71
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
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
|
===================================
DrNim User Guide
===================================
:Author: Andreas Rumpf
:Version: |nimversion|
.. contents::
Introduction
============
This document describes the usage of the *DrNim* tool. DrNim combines
the Nim frontend with the `Z3 <https://github.com/Z3Prover/z3>`_ proof
engine, in order to allow verify/validate software written in Nim.
DrNim's command-line options are the same as the Nim compiler's.
DrNim currently only checks the sections of your code that are marked
via ``staticBoundChecks: on``:
.. code-block:: nim
{.push staticBoundChecks: on.}
# <--- code section here ---->
{.pop.}
DrNim currently only tries to prove array indexing or subrange checks,
overflow errors are *not* prevented. Overflows will be checked for in
the future.
Later versions of the **Nim compiler** will **assume** that the checks inside
the ``staticBoundChecks: on`` environment have been proven correct and so
it will **omit** the runtime checks. If you do not want this behavior, use
instead ``{.push staticBoundChecks: defined(nimDrNim).}``. This way the
Nim compiler remains unaware of the performed proofs but DrNim will prove
your code.
Installation
============
Run ``koch drnim``, the executable will afterwards be in ``$nim/bin/drnim``.
Motivating Example
==================
The follow example highlights what DrNim can easily do, even
without additional annotations:
.. code-block:: nim
{.push staticBoundChecks: on.}
proc sum(a: openArray[int]): int =
for i in 0..a.len:
result += a[i]
{.pop.}
echo sum([1, 2, 3])
This program contains a famous "index out of bounds" bug. DrNim
detects it and produces the following error message::
cannot prove: i <= len(a) + -1; counter example: i -> 0 a.len -> 0 [IndexCheck]
In other words for ``i == 0`` and ``a.len == 0`` (for example!) there would be
an index out of bounds error.
Pre-, postconditions and invariants
===================================
DrNim adds 4 additional annotations (pragmas) to Nim:
- `requires`:idx:
- `ensures`:idx:
- `invariant`:idx:
- `assume`:idx:
These pragmas are ignored by the Nim compiler so that they don't have to
be disabled via ``when defined(nimDrNim)``.
Invariant
---------
An ``invariant`` is a proposition that must be true after every loop
iteration, it's tied to the loop body it's part of.
Requires
--------
A ``requires`` annotation describes what the function expects to be true
before it's called so that it can perform its operation. A ``requires``
annotation is also called a `precondition`:idx:.
Ensures
-------
An ``ensures`` annotation describes what will be true after the function
call. An ``ensures`` annotation is also called a `postcondition`:idx:.
Assume
------
An ``assume`` annotation describes what DrNim should **assume** to be true
in this section of the program. It is an unsafe escape mechanism comparable
to Nim's ``cast`` statement. Use it only when you really know better
than DrNim. You should add a comment to a paper that proves the proposition
you assume.
Example: insertionSort
======================
**Note**: This example does not yet work with DrNim.
.. code-block:: nim
import std / logic
proc insertionSort(a: var openArray[int]) {.
ensures: forall(i in 1..<a.len, a[i-1] <= a[i]).} =
for k in 1 ..< a.len:
{.invariant: 1 <= k and k <= a.len.}
{.invariant: forall(j in 1..<k, i in 0..<j, a[i] <= a[j]).}
var t = k
while t > 0 and a[t-1] > a[t]:
{.invariant: k < a.len.}
{.invariant: 0 <= t and t <= k.}
{.invariant: forall(j in 1..k, i in 0..<j, j == t or a[i] <= a[j]).}
swap a[t], a[t-1]
dec t
Unfortunately, the invariants required to prove that this code is correct take more
code than the imperative instructions. However, this effort can be compensated
by the fact that the result needs very little testing. Be aware though that
DrNim only proves that after ``insertionSort`` this condition holds::
forall(i in 1..<a.len, a[i-1] <= a[i])
This is required, but not sufficient to describe that a ``sort`` operation
was performed. For example, the same postcondition is true for this proc
which doesn't sort at all:
.. code-block:: nim
import std / logic
proc insertionSort(a: var openArray[int]) {.
ensures: forall(i in 1..<a.len, a[i-1] <= a[i]).} =
# does not sort, overwrites `a`'s contents!
for i in 0..<a.len: a[i] = i
Syntax of propositions
======================
The basic syntax is ``ensures|requires|invariant: <prop>``.
A ``prop`` is either a comparison or a compound::
prop = nim_bool_expression
| prop 'and' prop
| prop 'or' prop
| prop '->' prop # implication
| prop '<->' prop
| 'not' prop
| '(' prop ')' # you can group props via ()
| forallProp
| existsProp
forallProp = 'forall' '(' quantifierList ',' prop ')'
existsProp = 'exists' '(' quantifierList ',' prop ')'
quantifierList = quantifier (',' quantifier)*
quantifier = <new identifier> 'in' nim_iteration_expression
``nim_iteration_expression`` here is an ordinary expression of Nim code
that describes an iteration space, for example ``1..4`` or ``1..<a.len``.
``nim_bool_expression`` here is an ordinary expression of Nim code of
type ``bool`` like ``a == 3`` or ``23 > a.len``.
The supported subset of Nim code that can be used in these expressions
is currently underspecified but ``let`` variables, function parameters
and ``result`` (which represents the function's final result) are amenable
for verification. The expressions must not have any side-effects and must
terminate.
The operators ``forall``, ``exists``, ``->``, ``<->`` have to imported
from ``std / logic``.
|