examples/tests-provers/bv.why

   1 theory CheckBV64
   2   use bv.BV64
   3   use int.Int as Int
   4
   5   constant one   : t                                         = 1
   6   constant two   : t                                         = 2
   7   constant sz    : int                                       = 64
   8   constant mx    : int                                       = 0xFFFF_FFFF_FFFF_FFFF
   9   constant md    : int                                       = 0x1_0000_0000_0000_0000
  10   constant lastb : t                                         = 0x8000_0000_0000_0000
  11
  12   goal ok_zero   : zeros                                     = (0:t)
  13   goal ok_ones   : ones                                      = (of_int mx)
  14   goal ok_zero2  : t'int zeros                               = 0
  15   goal ok_ones2  : t'int ones                                = mx
  16   goal ok_size   : size                                      = sz
  17   goal ok_max    : t'maxInt                                     = mx
  18   goal ok_tpsize : two_power_size                            = md
  19
  20   goal ok1       : add ones one                              = zeros
  21   goal ok2       : sub zeros one                             = ones
  22   goal ok3       : neg ones                                  = one
  23   goal ok5       : mul one two                               = two
  24   goal ok6       : mul ones ones                             = one
  25   goal ok7       : udiv one two                              = zeros
  26   goal ok8       : urem one two                              = one
  27   goal ok9       : lsl_bv one one                            = two
  28   goal ok10      : lsl_bv ones one                           = sub ones one
  29   goal ok12      : lsr_bv one two                            = zeros
  30   goal ok13      : lsr_bv ones (sub (of_int sz) one)         = one
  31   goal ok14      : asr_bv one two                            = zeros
  32   goal ok15      : asr_bv ones two                           = ones
  33   goal ok16      : bw_and ones one                           = one
  34   goal ok17      : bw_or  ones one                           = ones
  35   goal ok18      : bw_xor ones one                           = sub ones one
  36   goal ok19      : bw_not ones                               = zeros
  37   goal ok20      : rotate_right_bv one one                   = lastb
  38   goal ok21      : rotate_right_bv ones two                  = ones
  39   goal ok22      : rotate_left_bv lastb one                  = one
  40   goal ok23      : rotate_left_bv ones two                   = ones
  41   goal ok24      : lsl_bv one (add (of_int sz) one)          = zeros
  42   goal ok25      : lsr_bv lastb (add (of_int sz) one)        = zeros
  43   goal ok26      : asr_bv lastb (add (of_int sz) one)        = ones
  44   goal ok27      : rotate_right_bv one (add (of_int sz) one) = lastb
  45   goal ok28      : rotate_left_bv one (add (of_int sz) one)  = two
  46
  47   goal trap      : of_int md                                 = zeros
  48
  49   goal smoke1    : neg lastb                                 = zeros
  50   goal smoke2    : udiv one zeros                            = zeros
  51   goal smoke3    : urem one zeros                            = zeros
  52   goal smoke4    : lsl_bv ones one                           = ones
  53   goal smoke5    : ugt (lsr_bv ones one) lastb
  54   goal smoke6    : ule (asr_bv lastb one) lastb
  55   goal smoke7    : rotate_right_bv one one                   = zeros
  56   goal smoke8    : rotate_left_bv lastb one                  = zeros
  57
  58   (* from example/logic/bitvectors.why *)
  59
  60   constant b0000  : t                                        = 0b0000
  61   constant b0001  : t                                        = 0b0001
  62   constant b0010  : t                                        = 0b0010
  63   constant b0011  : t                                        = 0b0011
  64   constant b0110  : t                                        = 0b0110
  65   constant b0101  : t                                        = 0b0101
  66   constant b0111  : t                                        = 0b0111
  67   constant b1100  : t                                        = 0b1100
  68   constant b11100 : t                                        = 0b11100
  69
  70   constant size_sub_one : int                                = Int.(-) size 1
  71
  72   goal g1 : bw_and b0011 b0110                               = b0010
  73   goal f1 : bw_and b0011 b0110                               = b0011
  74
  75   goal g2 :  bw_or b0011 b0110                               = b0111
  76   goal f2 :  bw_or b0011 b0110                               = b0110
  77
  78   goal g3 :  bw_xor b0011 b0110                              = b0101
  79   goal g4 :  bw_not b0011                                    = (0xFFFFFFFFFFFFFFFC:t)
  80
  81   goal g3a : lsr_bv b0111 (2:t)                              = b0001
  82   goal g3b : lsr_bv ones (of_int size_sub_one)               = b0001
  83   goal f3  : lsr_bv ones (0x100000001:t)                     = (0x7FFFFFFF:t)
  84
  85   goal g4a : lsl_bv b0111 (2:t)                              = b11100
  86   goal g4b : lsl_bv b0001 (31:t)                             = (0x80000000:t)
  87
  88   goal g5a : asr_bv b0111 (2:t)                              = b0001
  89   goal g5b : asr_bv ones (of_int (Int.(-) size 1))           = ones
  90
  91   goal g7 : t'int b11100                                   = 28
  92   goal f7 : t'int ones                                     = Int.(-_) 1
  93
  94   goal g8a : nth_bv b0110 (2:t)                              = True
  95   goal g8b : nth_bv b0110 (3:t)                              = False
  96
  97   goal Nth_Bv_bw_and:
  98     forall v1 v2 n. ult n size_bv ->
  99       nth_bv (bw_and v1 v2) n                                = andb (nth_bv v1 n) (nth_bv v2 n)
 100
 101   goal Nth_Bv_bw_or:
 102     forall v1 v2 n. ult n size_bv ->
 103       nth_bv (bw_or v1 v2) n                                 = orb (nth_bv v1 n) (nth_bv v2 n)
 104
 105   goal Nth_Bv_bw_xor:
 106     forall v1 v2 n. ult n size_bv ->
 107       nth_bv (bw_xor v1 v2) n                                = xorb (nth_bv v1 n) (nth_bv v2 n)
 108
 109   goal Nth_Bv_bw_not:
 110     forall v n. ult n size_bv ->
 111       nth_bv (bw_not v) n                                    = notb (nth_bv v n)
 112
 113   goal not_not : forall v:t. bw_not (bw_not v)               = v
 114
 115   goal not_and : forall v1 v2:t.
 116     bw_not (bw_and v1 v2)                                    = bw_or (bw_not v1) (bw_not v2)
 117
 118   goal Lsr_Bv_nth_bv_low: forall b n s.
 119     ult s size_bv -> ult n size_bv -> ult (add n s) size_bv ->
 120       nth_bv (lsr_bv b s) n                                  = nth_bv b (add n s)
 121
 122   goal Lsr_Bv_nth_bv_high: forall b n s.
 123     ult s size_bv -> ult n size_bv -> uge (add n s) size_bv ->
 124       nth_bv (lsr_bv b s) n                                  = False
 125
 126   goal Asr_Bv_nth_bv_low: forall b n s.
 127     ult s size_bv -> ult n size_bv -> ult (add n s) size_bv ->
 128        nth_bv (asr_bv b s) n                                 = nth_bv b (add n s)
 129
 130   goal Asr_Bv_nth_bv_high: forall b n s.
 131     ult s size_bv -> ult n size_bv -> uge (add n s) size_bv ->
 132       nth_bv (asr_bv b s) n                                  = nth_bv b (sub size_bv one)
 133
 134   goal Lsl_Bv_nth_bv_high: forall b n s.
 135     ult s size_bv -> ult n size_bv -> ult (sub n s) size_bv ->
 136       nth_bv (lsl_bv b s) n                                  = nth_bv b (sub n s)
 137
 138   goal Lsl_Bv_nth_bv_low: forall b n s.
 139     ult s size_bv -> ult n size_bv -> uge (sub n s) size_bv ->
 140       nth_bv (lsl_bv b s) n                                  = False
 141
 142 end
 143
 144 theory CheckBV32
 145   use bv.BV32
 146   use int.Int as Int
 147
 148   constant one   : t                                         = 1
 149   constant two   : t                                         = 2
 150   constant sz    : int                                       = 32
 151   constant mx    : int                                       = 0xFFFFFFFF
 152   constant md    : int                                       = 0x100000000
 153   constant lastb : t                                         = 0x80000000
 154
 155   goal ok_zero   : zeros                                     = (0:t)
 156   goal ok_ones   : ones                                      = (of_int mx)
 157   goal ok_zero2  : t'int zeros                               = 0
 158   goal ok_ones2  : t'int ones                                = mx
 159   goal ok_size   : size                                      = sz
 160   goal ok_max    : t'maxInt                                     = mx
 161   goal ok_tpsize : two_power_size                            = md
 162
 163   goal ok1       : add ones one                              = zeros
 164   goal ok2       : sub zeros one                             = ones
 165   goal ok3       : neg ones                                  = one
 166   goal ok5       : mul one two                               = two
 167   goal ok6       : mul ones ones                             = one
 168   goal ok7       : udiv one two                              = zeros
 169   goal ok8       : urem one two                              = one
 170   goal ok9       : lsl_bv one one                            = two
 171   goal ok10      : lsl_bv ones one                           = sub ones one
 172   goal ok12      : lsr_bv one two                            = zeros
 173   goal ok13      : lsr_bv ones (sub (of_int sz) one)         = one
 174   goal ok14      : asr_bv one two                            = zeros
 175   goal ok15      : asr_bv ones two                           = ones
 176   goal ok16      : bw_and ones one                           = one
 177   goal ok17      : bw_or  ones one                           = ones
 178   goal ok18      : bw_xor ones one                           = sub ones one
 179   goal ok19      : bw_not ones                               = zeros
 180   goal ok20      : rotate_right_bv one one                   = lastb
 181   goal ok21      : rotate_right_bv ones two                  = ones
 182   goal ok22      : rotate_left_bv lastb one                  = one
 183   goal ok23      : rotate_left_bv ones two                   = ones
 184   goal ok24      : lsl_bv one (add (of_int sz) one)          = zeros
 185   goal ok25      : lsr_bv lastb (add (of_int sz) one)        = zeros
 186   goal ok26      : asr_bv lastb (add (of_int sz) one)        = ones
 187   goal ok27      : rotate_right_bv one (add (of_int sz) one) = lastb
 188   goal ok28      : rotate_left_bv one (add (of_int sz) one)  = two
 189
 190   goal trap      : of_int md                                 = zeros
 191
 192   goal smoke1    : neg lastb                                 = zeros
 193   goal smoke2    : udiv one zeros                            = zeros
 194   goal smoke3    : urem one zeros                            = zeros
 195   goal smoke4    : lsl_bv ones one                           = ones
 196   goal smoke5    : ugt (lsr_bv ones one) lastb
 197   goal smoke6    : ule (asr_bv lastb one) lastb
 198   goal smoke7    : rotate_right_bv one one                   = zeros
 199   goal smoke8    : rotate_left_bv lastb one                  = zeros
 200 end
 201
 202 theory CheckBV16
 203   use bv.BV16
 204   use int.Int as Int
 205
 206   constant one   : t                                         = 1
 207   constant two   : t                                         = 2
 208   constant sz    : int                                       = 16
 209   constant mx    : int                                       = 65535
 210   constant md    : int                                       = 65536
 211   constant lastb : t                                         = 32768
 212
 213   goal ok_zero   : zeros                                     = (0:t)
 214   goal ok_ones   : ones                                      = (of_int mx)
 215   goal ok_zero2  : t'int zeros                               = 0
 216   goal ok_ones2  : t'int ones                                = mx
 217   goal ok_size   : size                                      = sz
 218   goal ok_max    : t'maxInt                                     = mx
 219   goal ok_tpsize : two_power_size                            = md
 220
 221   goal ok1       : add ones one                              = zeros
 222   goal ok2       : sub zeros one                             = ones
 223   goal ok3       : neg ones                                  = one
 224   goal ok5       : mul one two                               = two
 225   goal ok6       : mul ones ones                             = one
 226   goal ok7       : udiv one two                              = zeros
 227   goal ok8       : urem one two                              = one
 228   goal ok9       : lsl_bv one one                            = two
 229   goal ok10      : lsl_bv ones one                           = sub ones one
 230   goal ok12      : lsr_bv one two                            = zeros
 231   goal ok13      : lsr_bv ones (sub (of_int sz) one)         = one
 232   goal ok14      : asr_bv one two                            = zeros
 233   goal ok15      : asr_bv ones two                           = ones
 234   goal ok16      : bw_and ones one                           = one
 235   goal ok17      : bw_or  ones one                           = ones
 236   goal ok18      : bw_xor ones one                           = sub ones one
 237   goal ok19      : bw_not ones                               = zeros
 238   goal ok20      : rotate_right_bv one one                   = lastb
 239   goal ok21      : rotate_right_bv ones two                  = ones
 240   goal ok22      : rotate_left_bv lastb one                  = one
 241   goal ok23      : rotate_left_bv ones two                   = ones
 242   goal ok24      : lsl_bv one (add (of_int sz) one)          = zeros
 243   goal ok25      : lsr_bv lastb (add (of_int sz) one)        = zeros
 244   goal ok26      : asr_bv lastb (add (of_int sz) one)        = ones
 245   goal ok27      : rotate_right_bv one (add (of_int sz) one) = lastb
 246   goal ok28      : rotate_left_bv one (add (of_int sz) one)  = two
 247
 248   goal trap      : of_int md                                 = zeros
 249
 250   goal smoke1    : neg lastb                                 = zeros
 251   goal smoke2    : udiv one zeros                            = zeros
 252   goal smoke3    : urem one zeros                            = zeros
 253   goal smoke4    : lsl_bv ones one                           = ones
 254   goal smoke5    : ugt (lsr_bv ones one) lastb
 255   goal smoke6    : ule (asr_bv lastb one) lastb
 256   goal smoke7    : rotate_right_bv one one                   = zeros
 257   goal smoke8    : rotate_left_bv lastb one                  = zeros
 258 end
 259
 260 theory CheckBV8
 261   use bv.BV8
 262   use int.Int as Int
 263
 264   constant one   : t                                         = 1
 265   constant two   : t                                         = 2
 266   constant sz    : int                                       = 8
 267   constant mx    : int                                       = 255
 268   constant md    : int                                       = 256
 269   constant lastb : t                                         = 128
 270
 271   goal ok_zero   : zeros                                     = (0:t)
 272   goal ok_ones   : ones                                      = (of_int mx)
 273   goal ok_zero2  : t'int zeros                               = 0
 274   goal ok_ones2  : t'int ones                                = mx
 275   goal ok_size   : size                                      = sz
 276   goal ok_max    : t'maxInt                                     = mx
 277   goal ok_tpsize : two_power_size                            = md
 278
 279   goal ok1       : add ones one                              = zeros
 280   goal ok2       : sub zeros one                             = ones
 281   goal ok3       : neg ones                                  = one
 282   goal ok5       : mul one two                               = two
 283   goal ok6       : mul ones ones                             = one
 284   goal ok7       : udiv one two                              = zeros
 285   goal ok8       : urem one two                              = one
 286   goal ok9       : lsl_bv one one                            = two
 287   goal ok10      : lsl_bv ones one                           = sub ones one
 288   goal ok12      : lsr_bv one two                            = zeros
 289   goal ok13      : lsr_bv ones (sub (of_int sz) one)         = one
 290   goal ok14      : asr_bv one two                            = zeros
 291   goal ok15      : asr_bv ones two                           = ones
 292   goal ok16      : bw_and ones one                           = one
 293   goal ok17      : bw_or  ones one                           = ones
 294   goal ok18      : bw_xor ones one                           = sub ones one
 295   goal ok19      : bw_not ones                               = zeros
 296   goal ok20      : rotate_right_bv one one                   = lastb
 297   goal ok21      : rotate_right_bv ones two                  = ones
 298   goal ok22      : rotate_left_bv lastb one                  = one
 299   goal ok23      : rotate_left_bv ones two                   = ones
 300   goal ok24      : lsl_bv one (add (of_int sz) one)          = zeros
 301   goal ok25      : lsr_bv lastb (add (of_int sz) one)        = zeros
 302   goal ok26      : asr_bv lastb (add (of_int sz) one)        = ones
 303   goal ok27      : rotate_right_bv one (add (of_int sz) one) = lastb
 304   goal ok28      : rotate_left_bv one (add (of_int sz) one)  = two
 305
 306   goal trap      : of_int md                                 = zeros
 307
 308   goal smoke1    : neg lastb                                 = zeros
 309   goal smoke2    : udiv one zeros                            = zeros
 310   goal smoke3    : urem one zeros                            = zeros
 311   goal smoke4    : lsl_bv ones one                           = ones
 312   goal smoke5    : ugt (lsr_bv ones one) lastb
 313   goal smoke6    : ule (asr_bv lastb one) lastb
 314   goal smoke7    : rotate_right_bv one one                   = zeros
 315   goal smoke8    : rotate_left_bv lastb one                  = zeros
 316 end
 317
 318
 319
 320
 321
 322 theory Extras
 323
 324   use bv.BV64
 325
 326   lemma mod_mult: forall x [@model] a [@model] b [@model].
 327       ule zeros x ->
 328       ult zeros a ->
 329       ult zeros b ->
 330       ule a (0xffff_ffff:t) ->
 331       ule b (0xffff_ffff:t) ->
 332       urem (urem x (mul a b)) a = urem x a
 333
 334
 335
 336 end