blob: 1bbb7e0df8eafe59028cafae4047f1fff2ce62a5 (
plain)
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
|
# Gobra deductive proofs
`insertion.go` and `selection.go` are **machine-checked** proofs that these
sorts are correct, verified by [Gobra](https://github.com/viperproject/gobra) —
ETH Zurich's deductive verifier for Go, which translates annotated Go to the
Viper intermediate language and discharges the proof obligations with the Z3 SMT
solver.
Unlike the TLA+ models (which check a hand-written abstraction) and the property
tests (which sample inputs), these verify the **actual Go source** for **all**
inputs. Gobra proves two things about each sort:
1. **Memory safety** — every index access is in bounds. The permission
invariants `forall k :: 0 <= k < len(a) ==> acc(&a[k])` carry write access to
every element through both loops; Go itself cannot prove the absence of
index-out-of-range panics, Gobra can.
2. **Ordering** — on return `a` is sorted ascending
(`forall p < q :: a[p] <= a[q]`), established via the loop invariants in the
annotations. Selection sort needs the stronger "every prefix element ≤ every
suffix element" invariant; insertion sort uses a "sorted except at the
in-flight index" invariant.
The **permutation** half of full correctness (output is a rearrangement of the
input) is intentionally left to the property tests and the paper proof in
[`docs/verification.md`](../docs/verification.md); proving it in Gobra needs
ghost multiset state and is noted there as future work.
## Why a separate, non-generic copy?
Gobra's support for Go generics and method-based abstractions is limited, so
this file is a deliberately monomorphized copy of `sort.Insertion`
([`sort/insertion.go`](../sort/insertion.go)): plain `[]int` instead of
`ds.ArrayList[V]`, and an inlined swap instead of the `.Swap` method. The
algorithm is otherwise identical.
## Running
Gobra is distributed as a container image (it bundles its own Z3, so no separate
solver install is needed). With `podman` (or `docker`):
```sh
podman pull ghcr.io/viperproject/gobra:latest
make verify-formal
```
or directly:
```sh
podman run --rm -v "$PWD/formal:/gobra/formal:z" \
ghcr.io/viperproject/gobra:latest \
-i /gobra/formal/insertion.go /gobra/formal/selection.go
```
Expected output ends with:
```
Gobra found 0 errors.
```
To convince yourself the proof is not vacuous, flip the inner comparison
`a[j] < a[j-1]` to `>` and re-run: Gobra reports
`Loop invariant might not be preserved`.
|
