The Matrix Reproved (Verification Pearl)

Abstract

In this paper we describe a complete solution for the first challenge of the VerifyThis 2016 competition held at the 18th ETAPS Forum. We present the proof of two variants for the multiplication of matrices: a naive version using three nested loops and the Strassen’s algorithm. The proofs are conducted using the Why3 platform for deductive program verification, and automated theorem provers to discharge proof obligations. In order to specify and prove the two multiplication algorithms, we develop a new Why3 theory of matrices and apply the proof by reflection methodology.

This work is partly supported by the Bware (ANR-12-INSE-0010, http://bware.lri.fr/) and VOCAL (ANR-15-CE25-008, https://vocal.lri.fr/) projects of the French national research organization (ANR) and by the Portuguese Foundation for the Sciences and Technology (grant FCT-SFRH/BD/99432/2014).

Appendices

A Challenge 1 Original Text

Consider the following pseudocode algorithm, which is naive implementation of matrix multiplication. For simplicity we assume that the matrices are square.

Tasks.

• 1. Provide a specification to describe the behaviour of this algorithm, and prove that it correctly implements its specification.

• 2. Show that matrix multiplication is associative, i.e., the order in which matrices are multiplied can be disregarded: $A(BC) = (AB)C$. To show this, you should write a program that performs the two different computations, and then prove that the result of the two computations is always the same.

• 3. [Optional, if time permits] In the literature, there exist many proposals for more efficient matrix multiplication algorithms. Strassen’s algorithm was one of the first. The key idea of the algorithm is to use a recursive algorithm that reduces the number of multiplications on submatrices (from 8 to 7), see Strassen_algorithm on wikipedia for an explanation. A relatively clean Java implementation (and Python and C++) can be found here. Prove that the naive algorithm above has the same behaviour as Strassen’s algorithm. Proving it for a restricted case, like a $2\times 2$ matrix should be straightforward, the challenge is to prove it for arbitrary matrices with size $2^n$.

B Strassen Recursion Scheme

Given three matrices A, B and $M=AB$ partitioned as:

$$\begin{aligned} \begin{array}{ccc} A= \left[ \begin{array}{c|c} A_{1,1} &{} A_{1,2}\\ \hline A_{2,1} &{} A_{2,2} \\ \end{array} \right] &{} B= \left[ \begin{array}{c|c} B_{1,1} &{} B_{1,2}\\ \hline B_{2,1} &{} B_{2,2} \\ \end{array} \right] &{} M= \left[ \begin{array}{c|c} M_{1,1} &{} M_{1,2}\\ \hline M_{2,1} &{} M_{2,2} \\ \end{array} \right] \end{array} \end{aligned}$$

Then we can compute the partition of M from the two others as follow:

$$\begin{aligned} \begin{array}{lllrll} M_{1,1} &{} = &{} X_1 + X_4 - X_5 + X_7 &{} M_{2,1} &{} = &{} X_2 + X_4 \\ M_{1,2} &{} = &{} X_3 + X_5 &{} M_{2,2} &{} = &{} X_1 - X_2 + X_3 + X_6 \\ \end{array} \end{aligned}$$

With

$$\begin{aligned} \begin{array}{llrlrlrl} X_1 &{} = &{} (A_{1,1}+A_{2,2})&{}(B_{1,1}+B_{2,2}) &{} X_2 &{} = &{} (A_{2,1}+A_{2,2})&{}B_{1,1} \\ X_3 &{} = &{} A_{1,1}&{}(B_{1,2}-B_{2,2}) &{} X_4 &{} = &{} A_{2,2}&{}(B_{2,1} - B_{1,1}) \\ X_5 &{} = &{} (A_{1,1}+A_{1,2})&{}B_{2,2} &{} X_6 &{} = &{} (A_{2,1}-A_{1,1})&{}(B_{1,1}+B_{1,2}) \\ X_7 &{} = &{} (A_{1,2} - A_{2,2})&{}(B_{2,1}+B_{2,2}) &{} &{} &{} &{} \end{array} \end{aligned}$$