## Binary multiplication

See this description on Wikipedia

Authors: Jean-Christophe Filliâtre

Topics: Arithmetic

Tools: Why3

see also the index (by topic, by tool, by reference, by year)

# Russian peasant multiplication

Multiply two integers a and b using only addition, multiplication by 2, and division by 2.

Note: this is exactly the same algorithm as exponentiation by squaring with power/*/1 being replaced by */+/0.

```module BinaryMultiplication

use mach.int.Int
use ref.Ref

let binary_mult (a b: int) : int
requires { b >= 0 }
ensures  { result = a * b }
= let x = ref a in
let y = ref b in
let z = ref 0 in
while !y <> 0 do
invariant { 0 <= !y }
invariant { !z + !x * !y = a * b }
variant   { !y }
if !y % 2 = 1 then z := !z + !x;
x := 2 * !x;
y := !y / 2
done;
!z

end

```

Now using machine integers.

Assuming that the product fits in machine integers, we can still verify the code. The only exception is when `a*b = min_int`.

The code below makes no assumption on the sign of `b`. Instead, it uses the fact that `!y % 2` has the sign of `!y` so that `!x` is either added to or subtracted from the result.

```module BinaryMultiplication63

use int.Int
use int.Abs
use mach.int.Int63
use ref.Ref

let binary_mult (a b: int63) : int63
requires { min_int < a * b <= max_int }
ensures  { result = a * b }
= let x = ref a in
let y = ref b in
let z = ref 0 in
while !y <> 0 do
invariant { if a*b >= 0 then !x * !y >= 0 && !z >= 0
else !x * !y <= 0 && !z <= 0 }
invariant { !z + !x * !y = a * b }
variant   { abs !y }
z := !z + !x * (!y % 2);
y := !y / 2;
(* be careful not to make the very last multiplication *)
if !y <> 0 then x := 2 * !x
done;
!z

end
```

download ZIP archive

# Why3 Proof Results for Project "binary_multiplication"

## Theory "binary_multiplication.BinaryMultiplication": fully verified

 Obligations Alt-Ergo 2.1.0 VC for binary_mult 0.05

## Theory "binary_multiplication.BinaryMultiplication63": fully verified

 Obligations CVC4 1.5 VC for binary_mult --- split_vc loop invariant init 0.01 loop invariant init 0.00 division by zero 0.00 integer overflow 0.02 integer overflow 0.08 integer overflow 0.07 division by zero 0.00 integer overflow 0.01 integer overflow 0.22 loop variant decrease 0.01 loop invariant preservation 0.17 loop invariant preservation 1.00 loop variant decrease 0.01 loop invariant preservation 0.08 loop invariant preservation 0.11 postcondition 0.00