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