Author: | Andreas Rumpf |
---|---|

Version: | 2.0.0 |

# Introduction

This document describes the usage of the *DrNim* tool. DrNim combines the Nim frontend with the 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`:

{.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:

{.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
- ensures
- invariant
- assume

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.

## Ensures

An `ensures` annotation describes what will be true after the function call. An `ensures` annotation is also called a postcondition.

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

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:

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