tests/test_range.mlw

   1 theory T
   2   use int.Int
   3
   4   type q
   5
   6   type t is range t2int: 0 .. 42
   7
   8   (* meta "range:keep" type t *)
   9
  10   goal g : forall x:t. x = (12 : t)
  11 end
  12
  13 theory U
  14   use bv.BV8
  15
  16   type q
  17
  18   (* meta "range:keep" type t *)
  19
  20   goal g : forall x:t. x = (12 : t)
  21 end
  22
  23 module M
  24   use bv.BV16
  25   use int.Int
  26
  27   let f (x : t) : t
  28    ensures { ule result (12 : t) }
  29   = bw_and x (12 : t)
  30
  31 end
  32
  33 module N
  34   use bv.BV8
  35   use int.Int
  36
  37   use int.NumOf
  38
  39   meta "encoding : kept" type t
  40
  41   let ghost step1 (n x1 : t) (i : int) : unit
  42   =
  43     assert { let i' = of_int i in
  44              let twoi = mul (2 : t) i' in
  45                  to_uint (bw_and (lsr_bv x1 twoi) (0x03 : t))
  46                = numof (nth n) (to_uint twoi) (to_uint twoi + 2) }
  47
  48 end