examples/rightmostbittrick.mlw

   1 module Rmbt
   2   use int.Int
   3   use ref.Ref
   4   use bv.BV64
   5
   6   let ghost rightmost_position_set (a : t) : t
   7     requires { a <> zeros }
   8     ensures  { ult result (64:t) }
   9     ensures  { eq_sub_bv a zeros zeros result }
  10     ensures  { nth_bv a result }
  11   =
  12     let i = ref zeros in
  13     while ult !i (64:t) && not (nth_bv a !i) do
  14       variant {64 - t'int !i}
  15       invariant {eq_sub_bv a zeros zeros !i}
  16       i := add !i BV64.one
  17     done;
  18     !i
  19
  20   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     ensures  { eq_sub result zeros 0 !p }
  27     ensures  { eq_sub result zeros (!p+1) (63 - !p) }
  28     ensures  { nth result !p }
  29   =
  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     let r = bw_and x (neg x) in
  34     assert  { eq_sub_bv r zeros (add p_bv (1:t)) (sub (63:t) p_bv) };
  35     r
  36
  37 end