bitvector_TestBv32_to_int_0x80000000_1.v 6.36 KB
Newer Older
MARCHE Claude's avatar
MARCHE Claude committed
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below    *)
Require Import ZArith.
Require Import Rbase.
Parameter bv : Type.

Parameter nth: bv -> Z -> bool.


Parameter bvzero: bv.


Axiom Nth_zero : forall (n:Z), ((0%Z <= n)%Z /\ (n <  32%Z)%Z) ->
  ((nth bvzero n) = false).

Parameter bvone: bv.


Axiom Nth_one : forall (n:Z), ((0%Z <= n)%Z /\ (n <  32%Z)%Z) -> ((nth bvone
  n) = true).

Definition eq(v1:bv) (v2:bv): Prop := forall (n:Z), ((0%Z <= n)%Z /\
  (n <  32%Z)%Z) -> ((nth v1 n) = (nth v2 n)).

Axiom extensionality : forall (v1:bv) (v2:bv), (eq v1 v2) -> (v1 = v2).

Parameter bw_and: bv -> bv -> bv.


Axiom Nth_bw_and : forall (v1:bv) (v2:bv) (n:Z), ((0%Z <= n)%Z /\
  (n <  32%Z)%Z) -> ((nth (bw_and v1 v2) n) = (andb (nth v1 n) (nth v2 n))).

Parameter bw_or: bv -> bv -> bv.


Axiom Nth_bw_or : forall (v1:bv) (v2:bv) (n:Z), ((0%Z <= n)%Z /\
  (n <  32%Z)%Z) -> ((nth (bw_or v1 v2) n) = (orb (nth v1 n) (nth v2 n))).

Parameter bw_xor: bv -> bv -> bv.


Axiom Nth_bw_xor : forall (v1:bv) (v2:bv) (n:Z), ((0%Z <= n)%Z /\
  (n <  32%Z)%Z) -> ((nth (bw_xor v1 v2) n) = (xorb (nth v1 n) (nth v2 n))).

Parameter bw_not: bv -> bv.


Axiom Nth_bw_not : forall (v:bv) (n:Z), ((0%Z <= n)%Z /\ (n <  32%Z)%Z) ->
  ((nth (bw_not v) n) = (negb (nth v n))).

Parameter lsr: bv -> Z -> bv.


Axiom lsr_nth_low : forall (b:bv) (n:Z) (s:Z), ((0%Z <= n)%Z /\
  (n <  32%Z)%Z) -> ((0%Z <= s)%Z -> (((n + s)%Z <  32%Z)%Z -> ((nth (lsr b
  s) n) = (nth b (n + s)%Z)))).

Axiom lsr_nth_high : forall (b:bv) (n:Z) (s:Z), ((0%Z <= n)%Z /\
  (n <  32%Z)%Z) -> ((0%Z <= s)%Z -> ((32%Z <= (n + s)%Z)%Z -> ((nth (lsr b
  s) n) = false))).

Parameter asr: bv -> Z -> bv.


Axiom asr_nth_low : forall (b:bv) (n:Z) (s:Z), ((0%Z <= n)%Z /\
  (n <  32%Z)%Z) -> ((0%Z <= s)%Z -> (((n + s)%Z <  32%Z)%Z -> ((nth (asr b
  s) n) = (nth b (n + s)%Z)))).

Axiom asr_nth_high : forall (b:bv) (n:Z) (s:Z), ((0%Z <= n)%Z /\
  (n <  32%Z)%Z) -> ((0%Z <= s)%Z -> ((32%Z <= (n + s)%Z)%Z -> ((nth (asr b
  s) n) = (nth b (32%Z - 1%Z)%Z)))).

Parameter lsl: bv -> Z -> bv.


Axiom lsl_nth_high : forall (b:bv) (n:Z) (s:Z), ((0%Z <= n)%Z /\
  (n <  32%Z)%Z) -> ((0%Z <= s)%Z -> ((0%Z <= (n - s)%Z)%Z -> ((nth (lsl b s)
  n) = (nth b (n - s)%Z)))).

Axiom lsl_nth_low : forall (b:bv) (n:Z) (s:Z), ((0%Z <= n)%Z /\
  (n <  32%Z)%Z) -> ((0%Z <= s)%Z -> (((n - s)%Z <  0%Z)%Z -> ((nth (lsl b s)
  n) = false))).

Parameter to_nat_aux: bv -> Z -> Z.


Axiom to_nat_aux_zero : forall (b:bv) (i:Z), ((0%Z <= i)%Z /\
  (i <  32%Z)%Z) -> (((nth b i) = false) -> ((to_nat_aux b
  i) = (2%Z * (to_nat_aux b (i + 1%Z)%Z))%Z)).

Axiom to_nat_aux_one : forall (b:bv) (i:Z), ((0%Z <= i)%Z /\
  (i <  32%Z)%Z) -> (((nth b i) = true) -> ((to_nat_aux b
  i) = (1%Z + (2%Z * (to_nat_aux b (i + 1%Z)%Z))%Z)%Z)).

Axiom to_nat_aux_high : forall (b:bv) (i:Z), (32%Z <= i)%Z -> ((to_nat_aux b
  i) = 0%Z).

Parameter to_int_aux: bv -> Z -> Z.


Axiom to_int_aux_zero : forall (b:bv) (i:Z), ((0%Z <= i)%Z /\
  (i <  (32%Z - 1%Z)%Z)%Z) -> (((nth b i) = false) -> ((to_int_aux b
  i) = (2%Z * (to_int_aux b (i + 1%Z)%Z))%Z)).

Axiom to_int_aux_one : forall (b:bv) (i:Z), ((0%Z <= i)%Z /\
  (i <  (32%Z - 1%Z)%Z)%Z) -> (((nth b i) = true) -> ((to_int_aux b
  i) = (1%Z + (2%Z * (to_int_aux b (i + 1%Z)%Z))%Z)%Z)).

Axiom to_int_aux_pos : forall (b:bv), ((nth b (32%Z - 1%Z)%Z) = false) ->
  ((to_int_aux b (32%Z - 1%Z)%Z) = 0%Z).

Axiom to_int_aux_neg : forall (b:bv), ((nth b (32%Z - 1%Z)%Z) = true) ->
  ((to_int_aux b (32%Z - 1%Z)%Z) = (-1%Z)%Z).

(* YOU MAY EDIT THE CONTEXT BELOW *)

(* DO NOT EDIT BELOW *)

Theorem to_int_0x80000000 : ((to_int_aux (lsl bvone 31%Z)
  0%Z) = (-2147483648%Z)%Z).
(* YOU MAY EDIT THE PROOF BELOW *)
rewrite to_int_aux_zero; auto with zarith.
2: rewrite lsl_nth_low; auto with zarith.
rewrite to_int_aux_zero; auto with zarith.
2: rewrite lsl_nth_low; auto with zarith.
rewrite to_int_aux_zero; auto with zarith.
2: rewrite lsl_nth_low; auto with zarith.
rewrite to_int_aux_zero; auto with zarith.
2: rewrite lsl_nth_low; auto with zarith.
rewrite to_int_aux_zero; auto with zarith.
2: rewrite lsl_nth_low; auto with zarith.
rewrite to_int_aux_zero; auto with zarith.
2: rewrite lsl_nth_low; auto with zarith.
rewrite to_int_aux_zero; auto with zarith.
2: rewrite lsl_nth_low; auto with zarith.
rewrite to_int_aux_zero; auto with zarith.
2: rewrite lsl_nth_low; auto with zarith.
rewrite to_int_aux_zero; auto with zarith.
2: rewrite lsl_nth_low; auto with zarith.
rewrite to_int_aux_zero; auto with zarith.
2: rewrite lsl_nth_low; auto with zarith.
rewrite to_int_aux_zero; auto with zarith.
2: rewrite lsl_nth_low; auto with zarith.
rewrite to_int_aux_zero; auto with zarith.
2: rewrite lsl_nth_low; auto with zarith.
rewrite to_int_aux_zero; auto with zarith.
2: rewrite lsl_nth_low; auto with zarith.
rewrite to_int_aux_zero; auto with zarith.
2: rewrite lsl_nth_low; auto with zarith.
rewrite to_int_aux_zero; auto with zarith.
2: rewrite lsl_nth_low; auto with zarith.
rewrite to_int_aux_zero; auto with zarith.
2: rewrite lsl_nth_low; auto with zarith.
rewrite to_int_aux_zero; auto with zarith.
2: rewrite lsl_nth_low; auto with zarith.
rewrite to_int_aux_zero; auto with zarith.
2: rewrite lsl_nth_low; auto with zarith.
rewrite to_int_aux_zero; auto with zarith.
2: rewrite lsl_nth_low; auto with zarith.
rewrite to_int_aux_zero; auto with zarith.
2: rewrite lsl_nth_low; auto with zarith.
rewrite to_int_aux_zero; auto with zarith.
2: rewrite lsl_nth_low; auto with zarith.
rewrite to_int_aux_zero; auto with zarith.
2: rewrite lsl_nth_low; auto with zarith.
rewrite to_int_aux_zero; auto with zarith.
2: rewrite lsl_nth_low; auto with zarith.
rewrite to_int_aux_zero; auto with zarith.
2: rewrite lsl_nth_low; auto with zarith.
rewrite to_int_aux_zero; auto with zarith.
2: rewrite lsl_nth_low; auto with zarith.
rewrite to_int_aux_zero; auto with zarith.
2: rewrite lsl_nth_low; auto with zarith.
rewrite to_int_aux_zero; auto with zarith.
2: rewrite lsl_nth_low; auto with zarith.
rewrite to_int_aux_zero; auto with zarith.
2: rewrite lsl_nth_low; auto with zarith.
rewrite to_int_aux_zero; auto with zarith.
2: rewrite lsl_nth_low; auto with zarith.
rewrite to_int_aux_zero; auto with zarith.
2: rewrite lsl_nth_low; auto with zarith.
rewrite to_int_aux_zero; auto with zarith.
2: rewrite lsl_nth_low; auto with zarith.
rewrite to_int_aux_neg; auto with zarith.
rewrite lsl_nth_high; auto with zarith.
rewrite Nth_one; auto with zarith.
Qed.
(* DO NOT EDIT BELOW *)