Wiki Agenda Contact English version

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

  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)


download ZIP archive

Why3 Proof Results for Project "rightmostbittrick"

Theory "rightmostbittrick.Rmbt": fully verified

ObligationsAlt-Ergo 2.0.0CVC4 1.5Z3 4.6.0
VC rightmost_position_set---------
VC rightmost_position_set.00.02------
VC rightmost_position_set.10.20------
VC rightmost_position_set.20.09------
VC rightmost_position_set.3------0.04
VC rightmost_position_set.40.01------
VC rightmost_position_set.5------0.04
VC rightmost_bit_trick---------
VC rightmost_bit_trick.00.01------
VC rightmost_bit_trick.1------0.05
VC rightmost_bit_trick.20.02------
VC rightmost_bit_trick.30.07------
VC rightmost_bit_trick.40.04------
VC rightmost_bit_trick.50.28------
VC rightmost_bit_trick.6---0.47---
VC rightmost_bit_trick.70.10------