Commit 8645fe60 authored by MARCHE Claude's avatar MARCHE Claude

improved example rightmostbittrick: one assert less, 64 bit

parent 4730356d
module Rmbt
use import int.Int
use import ref.Ref
use import bv.BV32
use import bv.BV64
let ghost rightmost_position_set (a : t) : t
requires { a <> zero }
ensures { ult result (of_int 32) }
ensures { ult result (of_int 64) }
ensures { eq_sub_bv a zero zero result }
ensures { nth_bv a result }
=
let i = ref zero in
while ult !i (of_int 32) && not (nth_bv a !i) do
variant {32 - to_uint !i}
while ult !i (of_int 64) && not (nth_bv a !i) do
variant {64 - to_uint !i}
invariant {eq_sub_bv a zero zero !i}
i := add !i (of_int 1)
done;
......@@ -20,17 +20,16 @@ module Rmbt
let rightmost_bit_trick (x: t) (ghost p : ref int) : t
requires { x <> zero }
writes { p }
ensures { 0 <= !p < 32 }
ensures { 0 <= !p < 64 }
ensures { eq_sub x zero 0 !p }
ensures { nth x !p }
ensures { eq_sub result zero 0 !p }
ensures { eq_sub result zero (!p+1) 32 }
ensures { eq_sub result zero (!p+1) (63 - !p) }
ensures { nth result !p }
=
let ghost p_bv = rightmost_position_set x in
ghost p := to_uint p_bv;
assert { nth_bv (neg x) p_bv };
let res = bw_and x (neg x) in
assert {eq_sub_bv res zero (add p_bv (of_int 1)) (sub (of_int 31) p_bv )};
res
bw_and x (neg x)
end
\ No newline at end of file
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment