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.0.0
VC binary_mult0.05

Theory "binary_multiplication.BinaryMultiplication63": fully verified

ObligationsCVC4 1.5
VC binary_mult---
split_vc
VC binary_mult.00.01
VC binary_mult.10.00
VC binary_mult.20.00
VC binary_mult.30.02
VC binary_mult.40.08
VC binary_mult.50.07
VC binary_mult.60.00
VC binary_mult.70.01
VC binary_mult.80.22
VC binary_mult.90.01
VC binary_mult.100.17
VC binary_mult.110.73
VC binary_mult.120.01
VC binary_mult.130.08
VC binary_mult.140.11
VC binary_mult.150.00