VerifyThis Competition 2016: KIV Solutions

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.

Challenge 1: Matrix Multiplication

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

Project overview matrix.

Algebraic Part

Matrices are specified as a non-free data type

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

Program Verification

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]


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:

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.