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

Obligations | Alt-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 init | 0.05 | 0.01 | 0.02 | 0.58 | --- | --- | |

2. loop invariant preservation | --- | 0.15 | 0.07 | --- | 0.20 | --- | |

3. loop variant decrease | 0.12 | 0.06 | 0.02 | --- | --- | --- | |

4. postcondition | --- | 0.01 | --- | 0.00 | --- | --- | |

5. postcondition | 0.04 | 0.02 | 0.02 | 0.00 | --- | 0.00 | |

6. postcondition | 0.05 | 0.02 | 0.01 | 0.00 | --- | 0.00 | |

7. postcondition | --- | 0.01 | --- | --- | 0.04 | --- | |

8. postcondition | 0.05 | 0.01 | 0.02 | 0.00 | --- | 0.00 | |

9. postcondition | --- | 0.02 | --- | --- | 0.06 | --- | |

2. VC for rightmost_bit_trick | --- | --- | --- | --- | --- | --- | |

split_goal_wp | |||||||

1. precondition | 0.04 | 0.00 | 0.02 | 0.00 | --- | 0.00 | |

2. assertion | --- | 0.02 | --- | --- | --- | --- | |

3. postcondition | 0.07 | 0.02 | 0.03 | --- | --- | --- | |

4. postcondition | 0.02 | --- | 0.03 | --- | --- | --- | |

5. postcondition | 0.02 | --- | 0.02 | --- | --- | --- | |

6. postcondition | --- | 0.43 | --- | --- | --- | --- | |

7. postcondition | --- | 0.27 | --- | --- | --- | --- | |

8. postcondition | 0.15 | --- | 0.03 | --- | --- | --- |