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

References: ProofInUse joint laboratory

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 (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 in 0.00 s

ObligationsAlt-Ergo (1.01)CVC4 (1.4)CVC4 (1.4 noBV)Z3 (4.3.2)Z3 (4.5.0)Z3 (4.5.0 noBV)
1. VC for rightmost_position_set------------------
split_goal_wp
  1. loop invariant init0.050.010.020.58------
2. loop invariant preservation---0.150.07---0.20---
3. loop variant decrease0.120.060.02---------
4. postcondition---0.01---0.00------
5. postcondition0.040.020.020.00---0.00
6. postcondition0.050.020.010.00---0.00
7. postcondition---0.01------0.04---
8. postcondition0.050.010.020.00---0.00
9. postcondition---0.02------0.06---
2. VC for rightmost_bit_trick------------------
split_goal_wp
  1. precondition0.040.000.020.00---0.00
2. assertion---0.02------------
3. postcondition0.070.020.03---------
4. postcondition0.02---0.03---------
5. postcondition0.02---0.02---------
6. postcondition---0.43------------
7. postcondition---0.27------------
8. postcondition0.15---0.03---------