examples_in_progress/bit_reversal.mlw

   1
   2 module BitReversal
   3
   4   use int.Int
   5   use bv.BV32
   6   use array.Init
   7
   8
   9   let swap (a:array 'a) (i j : t)
  10     requires { 0 <= t'int i < a.length }
  11     requires { 0 <= t'int j < a.length }
  12     writes { a }
  13     ensures { a[t'int i] = old a[t'int j] }
  14     ensures { a[t'int j] = old a[t'int i] }
  15     ensures { forall k. 0 <= k < a.length ->
  16                 k <> t'int i /\ k <> t'int j -> a[k] = (old a)[k] }
  17   =
  18     let tmp = a[to_uint i] in
  19     a[to_uint i] <- a[to_uint j];
  20     a[to_uint j] <- tmp
  21
  22 (* a's size must be a power of two. *)
  23
  24   let rec aux (a:array t) (i di h hi:t)
  25     (ghost loglen masklen logdi loghi:t)
  26     requires { ult loglen (of_int 32) }
  27     requires { masklen = lsl_bv ones loglen }
  28     requires { a.length = t'int (lsl_bv (of_int 1) loglen) }
  29     requires { ult logdi (of_int 32) && di = lsl_bv (of_int 1) logdi }
  30     requires { ult loghi (of_int 32) && hi = lsl_bv (of_int 1) loghi }
  31     requires { t'int logdi + t'int loghi = t'int loglen }
  32     requires { t'int i < a.length }
  33     requires { t'int di <= a.length }
  34     requires { t'int h < a.length }
  35     requires { di <> of_int 0 }
  36     writes { a }
  37     variant { t'int di }
  38   =
  39    if eq di (of_int 1) then (if ult i h then swap a i h) else
  40     let dj = lsr_bv di (of_int 1) in
  41     let hj = lsl_bv hi (of_int 1) in
  42     assert { t'int logdi >= 1 };
  43     assert { ule dj (lsl_bv (of_int 1) (BV32.sub logdi (of_int 1))) };
  44     assert { bw_and dj masklen = zeros };
  45     assert { ult i (lsl_bv (of_int 1) loglen) };
  46     assert { bw_and i masklen = zeros };
  47     assert { ult h (lsl_bv (of_int 1) loglen) };
  48     assert { bw_and h masklen = zeros };
  49     aux a i dj h hj loglen masklen
  50       (BV32.sub logdi (of_int 1)) (BV32.add loghi (of_int 1));
  51     aux a (bw_or i dj) dj (bw_or h hi) hj loglen masklen
  52       (BV32.sub logdi (of_int 1)) (BV32.add loghi (of_int 1))
  53
  54 let bit_rev (a:array t) (ghost loglen:t)
  55   requires { ult loglen (of_int 32) && a.length = t'int (lsl_bv (of_int 1) loglen) }
  56   =
  57   aux a (of_int 0) (of_int a.length) (of_int 0) (of_int 1)
  58         loglen (lsl_bv ones loglen) loglen (of_int 0)
  59
  60
  61 let main () =
  62   let n = lsl_bv (of_int 1) (of_int 25) in
  63   let a = init (to_uint n) (fun i -> of_int i) in
  64   bit_rev a (of_int 25)
  65
  66
  67 end