Wiki Agenda Contact Version française

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.


Authors: Clément Fumex / Claude Marché

Topics: Ghost code / Bitwise operations

Tools: Why3

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


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

  let ghost rightmost_position_set (a : t) : t
    requires { a <> zeros }
    ensures  { ult result (of_int 64) }
    ensures  { eq_sub_bv a zeros zeros result }
    ensures  { nth_bv a result }
  =
    let i = ref zeros in
    while ult !i (of_int 64) && not (nth_bv a !i) do
      variant {64 - to_uint !i}
      invariant {eq_sub_bv a zeros zeros !i}
      i := add !i (of_int 1)
    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 := to_uint 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 in 3.19 s

ObligationsAlt-Ergo (0.99.1)CVC4 (1.4)CVC4 (1.4 noBV)Z3 (4.4.0)Z3 (4.4.0 noBV)
VC for rightmost_position_set---------------
split_goal_wp
  1. loop invariant init0.050.010.020.01---
2. loop invariant preservation---0.030.070.02---
3. loop variant decrease1.250.060.02------
4. postcondition---0.01---0.01---
5. postcondition0.040.020.020.000.00
6. postcondition0.050.020.010.000.00
7. postcondition---0.01---0.00---
8. postcondition0.050.010.020.000.00
9. postcondition---0.02---0.00---
VC for rightmost_bit_trick---------------
split_goal_wp
  1. precondition0.040.000.020.000.00
2. assertion---0.02---0.03---
3. postcondition0.070.020.03------
4. postcondition0.18---0.03------
5. postcondition0.02---0.02------
6. postcondition---0.43---------
7. postcondition---0.27---------
8. postcondition0.15---0.03------