Wiki Agenda Contact Version française

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

ObligationsAlt-Ergo 2.1.0
VC for binary_mult0.05

Theory "binary_multiplication.BinaryMultiplication63": fully verified

ObligationsCVC4 1.5
VC for binary_mult---
split_vc
loop invariant init0.01
loop invariant init0.00
division by zero0.00
integer overflow0.02
integer overflow0.08
integer overflow0.07
division by zero0.00
integer overflow0.01
integer overflow0.22
loop variant decrease0.01
loop invariant preservation0.17
loop invariant preservation1.00
loop variant decrease0.01
loop invariant preservation0.08
loop invariant preservation0.11
postcondition0.00