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

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

Project overview matrix.

Algebraic Part

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 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]

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

[Imprint] [Data Privacy Statement] [E-Mail]