test_range.mlw 718 Bytes
Newer Older
Clément Fumex's avatar
Clément Fumex committed
1
theory T
2
  use int.Int
Clément Fumex's avatar
Clément Fumex committed
3 4 5 6 7 8 9 10 11 12 13

  type q

  type t is range t2int: 0 .. 42

  (* meta "range:keep" type t *)

  goal g : forall x:t. x = (12 : t)
end

theory U
14
  use bv.BV8
Clément Fumex's avatar
Clément Fumex committed
15 16 17 18 19 20 21 22 23

  type q

  (* meta "range:keep" type t *)

  goal g : forall x:t. x = (12 : t)
end

module M
24 25
  use bv.BV16
  use int.Int
Clément Fumex's avatar
Clément Fumex committed
26 27 28 29 30 31 32 33

  let f (x : t) : t
   ensures { ule result (12 : t) }
  = bw_and x (12 : t)

end

module N
34 35
  use bv.BV8
  use int.Int
Clément Fumex's avatar
Clément Fumex committed
36

37
  use int.NumOf
Clément Fumex's avatar
Clément Fumex committed
38 39 40 41 42 43 44 45 46 47 48

  meta "encoding : kept" type t

  let ghost step1 (n x1 : t) (i : int) : unit
  =
    assert { let i' = of_int i in
             let twoi = mul (2 : t) i' in
                 to_uint (bw_and (lsr_bv x1 twoi) (0x03 : t))
               = numof (nth n) (to_uint twoi) (to_uint twoi + 2) }

end