rightmostbittrick.mlw 903 Bytes
Newer Older
1
module Rmbt
2 3 4
  use int.Int
  use ref.Ref
  use bv.BV64
5

6
  let ghost rightmost_position_set (a : t) : t
7
    requires { a <> zeros }
Clément Fumex's avatar
Clément Fumex committed
8
    ensures  { ult result (64:t) }
9
    ensures  { eq_sub_bv a zeros zeros result }
10 11
    ensures  { nth_bv a result }
  =
12
    let i = ref zeros in
Clément Fumex's avatar
Clément Fumex committed
13 14
    while ult !i (64:t) && not (nth_bv a !i) do
      variant {64 - t'int !i}
15
      invariant {eq_sub_bv a zeros zeros !i}
Clément Fumex's avatar
Clément Fumex committed
16
      i := add !i one
17 18 19 20
    done;
    !i

  let rightmost_bit_trick (x: t) (ghost p : ref int) : t
21
    requires { x <> zeros }
22
    writes   { p }
23
    ensures  { 0 <= !p < 64 }
24
    ensures  { eq_sub x zeros 0 !p }
25
    ensures  { nth x !p }
26 27
    ensures  { eq_sub result zeros 0 !p }
    ensures  { eq_sub result zeros (!p+1) (63 - !p) }
28 29
    ensures  { nth result !p }
  =
30
    let ghost p_bv = rightmost_position_set x in
31
    ghost p := t'int p_bv;
32
    assert { nth_bv (neg x) p_bv };
33 34
    bw_and x (neg x)

35
end