examples/tests/bv-smtlib-realization.why

   1
   2 (*
   3
   4 run this test with:
   5
   6 why3 ide -C ../../why3-smt-realize.conf -P cvc4r bv-smtlib-realization.why
   7
   8 *)
   9
  10 theory BV_Check
  11
  12   use int.Int
  13   use bv.BV8
  14
  15   goal size_pos : size > 0
  16
  17 (* Conversions from/to integers *)
  18
  19   use bv.Pow2int
  20
  21   lemma two_power_size_val : two_power_size = pow2 size
  22   lemma max_int_val : t'maxInt = two_power_size - 1
  23
  24   lemma to_uint_extensionality :
  25     forall v,v':t. t'int v = t'int v' -> v = v'
  26
  27   lemma to_int_extensionality:
  28     forall v,v':t. to_int v = to_int v' -> v = v'
  29
  30   lemma to_uint_bounds : forall v:t. 0 <= t'int v < two_power_size
  31
  32   lemma to_uint_of_int :
  33     forall i. 0 <= i < two_power_size -> t'int (of_int i) = i
  34
  35   lemma Of_int_zero: zeros = of_int 0
  36
  37   lemma Of_int_ones: ones = of_int t'maxInt
  38
  39   goal nth_out_of_bound:
  40     forall x n. size <= n <= t'maxInt -> nth x n = False
  41
  42   goal Nth_zero: forall n:int. 0 <= n < size -> nth zeros n = False
  43
  44   goal Nth_ones:
  45     (forall n. ult n size_bv -> nth_bv ones n = True) &&
  46     forall n. 0 <= n < size -> ult (of_int n) size_bv && nth ones n = True
  47
  48   (** Bitwise operators *)
  49
  50   goal Nth_bw_and:
  51     forall v1 v2:t, n:int. 0 <= n < size ->
  52       nth (bw_and v1 v2) n = andb (nth v1 n) (nth v2 n)
  53
  54   goal Nth_bw_or:
  55     forall v1 v2:t, n:int. 0 <= n < size ->
  56       nth (bw_or v1 v2) n = orb (nth v1 n) (nth v2 n)
  57
  58   goal Nth_bw_xor:
  59     forall v1 v2:t, n:int. 0 <= n < size ->
  60       nth (bw_xor v1 v2) n = xorb (nth v1 n) (nth v2 n)
  61
  62   goal Nth_bw_not:
  63     forall v:t, n:int. 0 <= n < size ->
  64       nth (bw_not v) n = notb (nth v n)
  65
  66   goal Lsr_nth_low:
  67     forall b:t,n s:int. 0 <= s -> 0 <= n -> n+s < size ->
  68       nth (lsr b s) n = nth b (n+s)
  69
  70   goal Lsr_nth_high:
  71     forall b:t,n s:int. 0 <= s -> 0 <= n -> n+s >= size ->
  72       nth (lsr b s) n = False
  73
  74   goal lsr_zero: forall x. lsr x 0 = x
  75
  76   goal Asr_nth_low:
  77     forall b:t,n s:int. 0 <= s -> 0 <= n < size -> n+s < size ->
  78       nth (asr b s) n = nth b (n+s)
  79
  80   goal Asr_nth_high:
  81     forall b:t,n s:int. 0 <= s -> 0 <= n < size -> n+s >= size ->
  82       nth (asr b s) n = nth b (size-1)
  83
  84   goal asr_zero: forall x. asr x 0 = x
  85
  86   goal Lsl_nth_high:
  87     forall b:t,n s:int. 0 <= s <= n < size ->
  88       nth (lsl b s) n = nth b (n-s)
  89
  90   goal Lsl_nth_low:
  91     forall b:t,n s:int. 0 <= n < s ->
  92       nth (lsl b s) n = False
  93
  94   goal lsl_zero: forall x. lsl x 0 = x
  95
  96   use int.EuclideanDivision
  97
  98   goal Nth_rotate_right :
  99     forall v n i. 0 <= i < size -> 0 <= n ->
 100       nth (rotate_right v n) i = nth v (mod (i + n) size)
 101
 102   goal Nth_rotate_left :
 103     forall v n i. 0 <= i < size -> 0 <= n ->
 104       nth (rotate_left v n) i = nth v (mod (i - n) size)
 105
 106
 107   (* comparison operators *)
 108
 109   goal ult_spec: forall x y. ult x y <-> Int.(<) (t'int x) (t'int y)
 110
 111   goal ule_spec: forall x y. ule x y <-> Int.(<=) (t'int x) (t'int y)
 112
 113   goal ugt_spec: forall x y. ugt x y <-> Int.(>) (t'int x) (t'int y)
 114
 115   goal uge_spec: forall x y. uge x y <-> Int.(>=) (t'int x) (t'int y)
 116
 117   goal slt_spec: forall x y. slt x y  <-> Int.(<) (to_int x) (to_int y)
 118
 119   goal sle_spec: forall x y. sle x y <-> Int.(<=) (to_int x) (to_int y)
 120
 121   goal sgt_spec: forall x y. sgt x y <-> Int.(>) (to_int x) (to_int y)
 122
 123   goal sge_spec: forall x y. sge x y <-> Int.(>=) (to_int x) (to_int y)
 124
 125   (** Arithmetic operators *)
 126
 127   goal to_uint_add:
 128     forall v1 v2. t'int (add v1 v2) =  mod (Int.(+) (t'int v1) (t'int v2)) two_power_size
 129   goal to_uint_add_bounded:
 130     forall v1 v2.
 131       t'int v1 + t'int v2 < two_power_size ->
 132       t'int (add v1 v2) = t'int v1 + t'int v2
 133
 134   goal to_uint_sub:
 135     forall v1 v2. t'int (sub v1 v2) = mod (Int.(-) (t'int v1) (t'int v2)) two_power_size
 136   goal to_uint_sub_bounded:
 137     forall v1 v2.
 138       0 <= t'int v1 - t'int v2 < two_power_size ->
 139       t'int (sub v1 v2) = t'int v1 - t'int v2
 140
 141   goal to_uint_neg:
 142     forall v. t'int (neg v) = mod (Int.(-_) (t'int v)) two_power_size
 143
 144   goal to_uint_mul:
 145     forall v1 v2. t'int (mul v1 v2) = mod (Int.( * ) (t'int v1) (t'int v2)) two_power_size
 146   goal to_uint_mul_bounded:
 147     forall v1 v2.
 148       t'int v1 * t'int v2 < two_power_size ->
 149       t'int (mul v1 v2) = t'int v1 * t'int v2
 150
 151   goal to_uint_udiv:
 152     forall v1 v2. t'int (udiv v1 v2) = div (t'int v1) (t'int v2)
 153
 154   goal to_uint_urem:
 155     forall v1 v2. t'int (urem v1 v2) = mod (t'int v1) (t'int v2)
 156
 157   goal to_uint_lsr:
 158     forall v n : t.
 159       t'int (lsr_bv v n) = div (t'int v) (pow2 ( t'int n ))
 160
 161   goal to_uint_lsl:
 162     forall v n : t.
 163          t'int (lsl_bv v n) = mod (Int.( * ) (t'int v) (pow2 (t'int n))) two_power_size
 164
 165   (* equality goals *)
 166
 167   goal eq_sub_equiv: forall a b i n:t.
 168       eq_sub    a b (t'int i) (t'int n)
 169   <-> eq_sub_bv a b i n
 170
 171   goal Extensionality: forall x y : t [x == y]. x == y -> x = y
 172
 173 end
 174
 175 theory BVConverter_Check
 176
 177   use bv.BVConverter_32_64
 178
 179   goal toSmall_to_uint :
 180     forall x. in_range x -> BV64.t'int x = BV32.t'int (toSmall x)
 181
 182   goal toBig_to_uint :
 183     forall x. BV32.t'int x = BV64.t'int (toBig x)
 184
 185 end