This page documents the KIV solutions of the VerifyThis Competition held at ETAPS 2016 in Eindhoven.

So far only challenge 1, the others might appear eventually.

The task was to specify matrix multiplication, verify a variant of the algorithm n³ algorithm, and prove that the operation is associative.

This solution is based on the ideas of the on-site version with two improvements

- a proper matrix data type is used instead of unbounded two-dimensional maps
- the solution is generalized to non-square matrices.

Project overview matrix.

Matrices are specified as a non-free data type

- the constructor
`m × n`

that constructs a matrix with`m`

rows and`n`

columns initialized to all`0`

entries - the dimensions of
`A`

can be retrieved as`A.rows`

and`A.cols`

- lookup is written
`A[i,j]`

and underspecified for indices out of bounds - The extensionality axiom specifies matrix equality in terms of the dimensions and lookup.

Dot-product is specified by

`(A * B)[m, n] = Σ(A.cols, λ k. A[m, k] * B[k, n])`

for indices in bounds and for two compatible matrices such that `A.cols = B.rows`

.

The summation operator `Σ(n, nf)`

takes a function `nf`

and produces the sum

`nf(0) + nf(1) + … + nf(n-1)`

The proof for associativity of matrix multiplication proceeds by extensionality, i.e., it is shown that lookup for each valid index of `(A * B) * C`

and `A * (B * C)`

produces the same result (and furthermore, that the resulting dimensions are correct).

The key step in the proof is lemma sum-swap

```
Σ(n, λ k0. Σ(m, λ k1. nnf(k0, k1)))
= Σ(m, λ k1. Σ(n, λ k0. nnf(k0, k1)))
```

that permits to swap the indices of two nested sums.

This lemma is proved by induction on `n`

(or `m`

alternatively).

- The base case follows from
`Σ(n, λ k. 0) = 0`

(lemma sum-empty) - The inductive case needs to split a summation into two parts
`Σ(n, λ k. nf0(k) + nf1(k)) = Σ(n, nf0) + Σ(n, nf1)`

(lemma sum-split)

Another critical property is distribution of multiplication over sums`i * Σ(n, nf) = Σ(n, λ k. i * nf(k))`

(lemma dist)

Program multiply implements matrix multiplication `A * B`

by three nested loops

```
C: A.rows × B.cols
for m = 0 .. A.rows do
for k = 0 .. A.cols do
for n = 0 .. B.cols do
C[m,n] += A[m,k] * B[k,n]
```

(pseudocode).

Correctness just states that the procedure terminates and that the output `C`

equals `A * B`

:

`A.cols = B.rows ⊦ ⟨multiply(A, B; C)⟩ (C = A * B)`

The invariants are contained in the program as annotations. The important parts are:

- Inner loop:
`C[m,n0]`

for`n0 < n`

contains`old(C)[m,n0] + A[m,k] * B[k,n0]`

already - The middle loop lifts
`C[m,n0]`

for`n0 < n`

to the sum`old(C)[m,n0] + Σ(k, λ k. A[m0, k] * B[k, n0])`

up to`k`

: - The outer loop generalizes this property to all
`m0 < m`

All other entries are unchanged.

To understand the concrete notation, e.g., for the inner loop

```
n ≤ C.cols ∧ C.rows = A.rows ∧ C.cols = B.cols
∧ ∀ m0, n0.
m0 < C.rows ∧ n0 < C.cols
→ C[m0, n0] = (C`)[m0, n0]
+ (m0 = m ∧ n0 < n
⊃ A[m0, k] * B[k, * n0]
; 0)
```

it should be noted that `C`

` stands the old value of `C`

from just before the first iteration of that particular loop; and `(test ⊃ x ; y)`

is an if-then-else formula/expression, i.e., some entries are incremented by the product, and some are (not) increment by `0`

.

The proof symbolically executes the program and solves the remaining predicate logic case distinctions and quantifier instantiations fully automatically.

Note that KIV propagates an instance of an outer invariant to an inner loop for the old values of the program variables mentioned, i.e., when the inner loop refers to `C`

` the middle invariant is known for this `C`

` and some even "older" value `C`

``, and so on to the top-level. For the example this is sufficiently strong so that one does not have to repeat the outer invariants as part of the inner loop.