## The rightmost bit trick

A smart and efficient code to compute the rightmost bit of a given bit vector. This case study is detailed in Inria research report 8821.

Auteurs: Clément Fumex / Claude Marché

Catégories: Ghost code / Bitwise operations

Outils: Why3

Références: ProofInUse joint laboratory

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

```module Rmbt
use int.Int
use ref.Ref
use bv.BV64

let ghost rightmost_position_set (a : t) : t
requires { a <> zeros }
ensures  { ult result (64:t) }
ensures  { eq_sub_bv a zeros zeros result }
ensures  { nth_bv a result }
=
let i = ref zeros in
while ult !i (64:t) && not (nth_bv a !i) do
variant {64 - t'int !i}
invariant {eq_sub_bv a zeros zeros !i}
i := add !i one
done;
!i

let rightmost_bit_trick (x: t) (ghost p : ref int) : t
requires { x <> zeros }
writes   { p }
ensures  { 0 <= !p < 64 }
ensures  { eq_sub x zeros 0 !p }
ensures  { nth x !p }
ensures  { eq_sub result zeros 0 !p }
ensures  { eq_sub result zeros (!p+1) (63 - !p) }
ensures  { nth result !p }
=
let ghost p_bv = rightmost_position_set x in
ghost p := t'int p_bv;
assert { nth_bv (neg x) p_bv };
bw_and x (neg x)

end```

download ZIP archive

# Why3 Proof Results for Project "rightmostbittrick"

## Theory "rightmostbittrick.Rmbt": fully verified

 Obligations Alt-Ergo 2.0.0 CVC4 1.5 Z3 4.6.0 VC rightmost_position_set --- --- --- split_goal_right VC rightmost_position_set.0 0.02 --- --- VC rightmost_position_set.1 0.20 --- --- VC rightmost_position_set.2 0.09 --- --- VC rightmost_position_set.3 --- --- 0.04 VC rightmost_position_set.4 0.01 --- --- VC rightmost_position_set.5 --- --- 0.04 VC rightmost_bit_trick --- --- --- split_goal_right VC rightmost_bit_trick.0 0.01 --- --- VC rightmost_bit_trick.1 --- --- 0.05 VC rightmost_bit_trick.2 0.02 --- --- VC rightmost_bit_trick.3 0.07 --- --- VC rightmost_bit_trick.4 0.04 --- --- VC rightmost_bit_trick.5 0.28 --- --- VC rightmost_bit_trick.6 --- 0.47 --- VC rightmost_bit_trick.7 0.10 --- ---