double_of_int.why 10.6 KB
 MARCHE Claude committed Apr 21, 2012 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 `````` theory DoubleOfInt use import int.Int use import bool.Bool use import real.RealInfix use import real.FromInt use power2.Pow2int use power2.Pow2real use bitvector.BV32 use bitvector.BV64 use bitvector.BV32_64 use import double.BV_double (*********************************************************************) (* j = 0x43300000 *) (* j' = 0x80000000 *) (*********************************************************************) function j : BV32.bv = BV32.from_int 0x43300000 `````` MARCHE Claude committed Feb 17, 2013 24 25 26 27 28 29 30 31 `````` lemma nth_j1: forall i:int. 0 <= i <= 19 -> BV32.nth j i = False lemma nth_j2: forall i:int. 20 <= i <= 21 -> BV32.nth j i = True lemma nth_j3: forall i:int. 22 <= i <= 23 -> BV32.nth j i = False lemma nth_j4: forall i:int. 24 <= i <= 25 -> BV32.nth j i = True lemma nth_j5: forall i:int. 26 <= i <= 29 -> BV32.nth j i = False lemma nth_j6: BV32.nth j 30 = True lemma nth_j7: BV32.nth j 31 = False `````` MARCHE Claude committed Apr 21, 2012 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 `````` function j' : BV32.bv = BV32.from_int 0x80000000 lemma jp0_30: forall i:int. 0<=i<30 -> BV32.nth j' i = False (*********************************************************************) (* definitions: *) (* const : bv64 = concat j j' *) (* const_as_double : real = double_of_bv64(const) *) (*********************************************************************) function const : BV64.bv = BV32_64.concat j j' function const_as_double : real = double_of_bv64 const (*********************************************************************) (* next lemma: const_as_double = 2^52 + 2^31 *) (*********************************************************************) lemma nth_const1: forall i:int. 0 <= i <= 30 -> BV64.nth const i = False lemma nth_const2: BV64.nth const 31 = True lemma nth_const3: forall i:int. 32 <= i <= 51 -> BV64.nth const i = False lemma nth_const4: forall i:int. 52 <= i <= 53 -> BV64.nth const i = True lemma nth_const5: forall i:int. 54 <= i <= 55 -> BV64.nth const i = False lemma nth_const6: forall i:int. 56 <= i <= 57 -> BV64.nth const i = True lemma nth_const7: forall i:int. 58 <= i <= 61 -> BV64.nth const i = False lemma nth_const8: BV64.nth const 62 = True lemma nth_const9: BV64.nth const 63 = False lemma sign_const: sign(const) = False lemma exp_const: exp(const) = 1075 lemma to_nat_mantissa_1: (BV64.to_nat_sub const 30 0) = 0 lemma mantissa_const_nth2: forall i:int. 32 <= i <= 51 -> BV64.nth const i = False lemma mantissa_const_to_nat51: BV64.to_nat_sub const 51 0 = BV64.to_nat_sub const 31 0 lemma mantissa_const: mantissa(const) = Pow2int.pow2 31 lemma real1075m1023: from_int (1075 - 1023) = 52.0 lemma real1075m1023_2: 1075.0 -. 1023.0 = 52.0 lemma real52_a_m52: Pow2real.pow2 (1075 - 1023) *. Pow2real.pow2 31 *. Pow2real.pow2 (-52) = Pow2real.pow2 31 lemma const_value0: const_as_double = 1.0*.Pow2real.pow2 (1075 - 1023) *. (1.0 +. Pow2real.pow2 31 *. Pow2real.pow2 (-52)) lemma const_value: const_as_double = Pow2real.pow2 52 +. Pow2real.pow2 31 (*********************************************************************) (* definitions: *) (* var(x) : bv64 = concat j (j' xor x) *) (* var_as_double(x) : real = double_of_bv64(var(x)) *) (*********************************************************************) function jpxor(i:int): BV32.bv = (BV32.bw_xor j' (BV32.from_int2c i)) function var(i:int): BV64.bv = (BV32_64.concat j (jpxor i)) function var_as_double(x:int) : real = double_of_bv64 (var x) (*********************************************************************) (* lemma 1: for all integer x, to_nat(jpxor(x)) = 2^31 + x *) (*********************************************************************) predicate is_int32(x:int) = - Pow2int.pow2 31 <= x < Pow2int.pow2 31 (* lemma two_compl_pos: forall x:int. is_int32 x /\ x >= 0 -> BV32.to_nat_sub (BV32.from_int2c x) 31 0 = x lemma two_compl_neg: forall x:int. is_int32 x /\ x < 0 -> BV32.to_nat_sub (BV32.from_int2c x) 31 0 = Pow2int.pow2 32 + x *) (* bits of jpxor x *) lemma nth_0_30: forall x:int. forall i:int. is_int32(x) /\ 0<=i<=30 -> BV32.nth (BV32.bw_xor j' (BV32.from_int2c x)) i = BV32.nth (BV32.from_int2c x) i lemma nth_jpxor_0_30: forall x:int. forall i:int. is_int32(x) /\ 0<=i<=30 -> BV32.nth (jpxor x) i = BV32.nth (BV32.from_int2c x) i lemma nth_var31: forall x:int. (BV32.nth (jpxor x) 31) = notb (BV32.nth (BV32.from_int2c x) 31) lemma to_nat_sub_0_30: forall x:int. is_int32(x) -> (BV32.to_nat_sub (BV32.bw_xor j' (BV32.from_int2c x)) 30 0) = (BV32.to_nat_sub (BV32.from_int2c x) 30 0) (* case x >= 0 *) lemma jpxorx_pos: forall x:int. x>=0 -> BV32.nth (BV32.bw_xor j' (BV32.from_int2c x)) 31 = True `````` MARCHE Claude committed May 24, 2012 124 `````` lemma from_int2c_to_nat_sub_pos: `````` Andrei Paskevich committed Oct 20, 2012 125 126 `````` forall i:int. 0 <= i <= 31 -> forall x:int. 0 <= x < Pow2int.pow2 i -> `````` MARCHE Claude committed May 24, 2012 127 128 `````` BV32.to_nat_sub (BV32.from_int2c x) (i-1) 0 = x `````` Andrei Paskevich committed Oct 20, 2012 129 `````` lemma lemma1_pos : forall x:int. is_int32 x /\ x >= 0 -> `````` MARCHE Claude committed May 24, 2012 130 131 132 133 `````` BV32.to_nat_sub (jpxor x) 31 0 = Pow2int.pow2 31 + x (* case x < 0 *) `````` Andrei Paskevich committed Oct 20, 2012 134 `````` lemma jpxorx_neg: forall x:int. x<0 -> `````` MARCHE Claude committed May 24, 2012 135 136 137 `````` BV32.nth (BV32.bw_xor j' (BV32.from_int2c x)) 31 = False lemma from_int2c_to_nat_sub_neg: `````` Andrei Paskevich committed Oct 20, 2012 138 139 `````` forall i:int. 0 <= i <= 31 -> forall x:int. -Pow2int.pow2 i <= x < 0 -> `````` MARCHE Claude committed May 24, 2012 140 `````` BV32.to_nat_sub (BV32.from_int2c x) (i-1) 0 = Pow2int.pow2 i + x `````` Andrei Paskevich committed Oct 20, 2012 141 142 `````` lemma lemma1_neg : forall x:int. is_int32 x /\ x < 0 -> `````` MARCHE Claude committed May 24, 2012 143 144 145 146 147 148 149 150 `````` BV32.to_nat_sub (jpxor x) 31 0 = Pow2int.pow2 31 + x (**** old (* case x >= 0 *) lemma jpxorx_pos: forall x:int. x>=0 -> BV32.nth (BV32.bw_xor j' (BV32.from_int2c x)) 31 = True `````` MARCHE Claude committed Apr 21, 2012 151 152 153 154 155 156 ``````(* lemma from_int2c_to_nat_sub31: forall x:int. x >= 0 -> BV32.to_nat_sub (BV32.from_int2c x) 31 0 = x *) lemma from_int2c_to_nat_sub_gen: `````` Andrei Paskevich committed Oct 20, 2012 157 158 `````` forall i:int. 0 <= i <= 30 -> forall x:int. 0 <= x < Pow2int.pow2 i -> `````` MARCHE Claude committed Apr 21, 2012 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 `````` BV32.to_nat_sub (BV32.from_int2c x) (i-1) 0 = x lemma from_int2c_to_nat_sub: forall x:int. is_int32(x) /\ x >= 0 -> BV32.to_nat_sub (BV32.from_int2c x) 30 0 = x lemma lemma1_pos : forall x:int. is_int32 x /\ x >= 0 -> BV32.to_nat_sub (jpxor x) 31 0 = Pow2int.pow2 31 + x (* case x < 0 *) lemma to_nat_sub_0_30_neg: forall x:int. is_int32(x) /\ x<0 -> (BV32.to_nat_sub (BV32.bw_xor j' (BV32.from_int2c x)) 30 0) = (BV32.to_nat_sub (BV32.from_int2c x) 30 0) lemma to_nat_sub_0_30_neg1: forall x:int. is_int32(x) /\ x<0 -> (BV32.to_nat_sub (BV32.from_int2c x) 30 0) = Pow2int.pow2 31 + x lemma lemma1_neg : forall x:int. is_int32 x /\ x < 0 -> BV32.to_nat_sub (jpxor x) 31 0 = Pow2int.pow2 31 + x `````` MARCHE Claude committed May 24, 2012 176 ``````****) `````` MARCHE Claude committed Apr 21, 2012 177 `````` `````` MARCHE Claude committed May 24, 2012 178 179 180 181 `````` (* final lemma *) lemma lemma1 : forall x:int. is_int32 x -> BV32.to_nat_sub (jpxor x) 31 0 = Pow2int.pow2 31 + x `````` MARCHE Claude committed Apr 21, 2012 182 183 184 185 186 187 188 189 190 191 `````` (*********************************************************************) (* lemma 2: for all integer x, mantissa(var(x)) = 2^31 + x *) (*********************************************************************) lemma nth_var_0_31: forall x:int. forall i:int. is_int32(x) /\ 0<=i<=31-> BV64.nth (var x) i = BV32.nth (jpxor x) i lemma to_nat_bv32_bv64_aux: forall b1:BV32.bv. forall b2:BV32.bv. forall j:int. 0<=j<32-> BV64.to_nat_sub (BV32_64.concat b1 b2) j 0 = BV32.to_nat_sub b2 j 0 lemma to_nat_bv32_bv64: forall b1:BV32.bv. forall b2:BV32.bv. BV64.to_nat_sub (BV32_64.concat b1 b2) 31 0 = BV32.to_nat_sub b2 31 0 `````` Andrei Paskevich committed Oct 20, 2012 192 `````` `````` MARCHE Claude committed Apr 21, 2012 193 194 195 196 197 `````` lemma to_nat_var_0_31: forall x:int. is_int32(x) -> BV64.to_nat_sub (var x) 31 0 = BV32.to_nat_sub (jpxor x) 31 0 lemma nth_var32to63: forall x k:int. 32 <= k <= 63 -> BV64.nth (var x) k = BV32.nth j (k - 32) `````` MARCHE Claude committed Feb 17, 2013 198 199 `````` lemma nth_var3: forall x i:int. is_int32 x /\ 32 <= i <= 51 -> BV64.nth (var x) i = False `````` Andrei Paskevich committed Oct 20, 2012 200 `````` `````` MARCHE Claude committed Apr 21, 2012 201 202 203 204 205 206 `````` lemma lemma2 : forall x:int. is_int32 x -> mantissa(var(x)) = Pow2int.pow2 31 + x (*********************************************************************) (* lemma 3: for all integer x, exp(var(x)) = 1075 *) (*********************************************************************) `````` MARCHE Claude committed Feb 17, 2013 207 208 209 210 211 212 213 214 `````` lemma nth_var4: forall x i:int. is_int32 x /\ 52 <= i <= 53 -> BV64.nth (var x) i = True lemma nth_var5: forall x i:int. is_int32 x /\ 54 <= i <= 55 -> BV64.nth (var x) i = False lemma nth_var6: forall x i:int. is_int32 x /\ 56 <= i <= 57 -> BV64.nth (var x) i = True `````` MARCHE Claude committed Apr 21, 2012 215 `````` `````` MARCHE Claude committed Feb 17, 2013 216 217 218 219 220 221 222 223 `````` lemma nth_var7: forall x i:int. is_int32 x /\ 58 <= i <= 61 -> BV64.nth (var x) i = False lemma nth_var8: forall x:int. is_int32 x -> BV64.nth (var x) 62 = True lemma lemma3 : forall x:int. is_int32 x -> exp(var(x)) = 1075 `````` MARCHE Claude committed Apr 21, 2012 224 225 226 227 228 `````` (*********************************************************************) (* lemma 4: for all integer x, sign(var(x)) = false *) (*********************************************************************) `````` MARCHE Claude committed Feb 17, 2013 229 230 `````` lemma nth_var9: forall x:int. is_int32 x -> BV64.nth (var x) 63 = False `````` MARCHE Claude committed Apr 21, 2012 231 `````` `````` MARCHE Claude committed Feb 17, 2013 232 233 `````` lemma lemma4 : forall x:int. is_int32 x -> sign(var(x)) = False `````` MARCHE Claude committed Apr 21, 2012 234 235 236 237 `````` (*********************************************************************) (* lemma 5: for all integer x, var_as_double(x) = 2^52 + 2^31 + x *) (*********************************************************************) `````` MARCHE Claude committed Feb 17, 2013 238 239 240 241 242 243 244 `````` lemma sign_var: forall x:int. is_int32 x -> sign(var(x)) = False (*proved by Coq*) lemma var_value0: forall x:int. is_int32(x) -> var_as_double(x) = Pow2real.pow2 (1075 - 1023) *. (1.0 +. (from_int (Pow2int.pow2 31 + x)) *. Pow2real.pow2 (-52)) `````` MARCHE Claude committed Apr 21, 2012 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 `````` lemma from_int_sum : forall x:int. is_int32(x)-> from_int (Pow2int.pow2 31 + x) = from_int (Pow2int.pow2 31) +. from_int x lemma var_value3: forall x:int. is_int32(x)->var_as_double(x) = Pow2real.pow2 52 +. Pow2real.pow2 52 *. (from_int (Pow2int.pow2 31) +. from_int x) *. Pow2real.pow2 (-52) lemma distr_pow52 : forall x:real. Pow2real.pow2 52 *. x *. Pow2real.pow2 (-52) = x lemma var_value4: forall x:int. is_int32(x)->var_as_double(x) = Pow2real.pow2 52 +. (from_int (Pow2int.pow2 31)) +. from_int x lemma pow31 : from_int (Pow2int.pow2 31) = Pow2real.pow2 31 lemma lemma5: forall x:int. is_int32(x)-> var_as_double(x) = Pow2real.pow2 52 +. Pow2real.pow2 31 +. (from_int x) (*********************************************************************) (* main result *) (*********************************************************************) function double_of_int32 (x:int) : real = var_as_double(x) -. const_as_double lemma MainResult: forall x:int. is_int32 x -> double_of_int32 x = from_int x end (* Local Variables: `````` MARCHE Claude committed Feb 27, 2015 281 ``````compile-command: "why3 ide -L . double_of_int.why" `````` MARCHE Claude committed Apr 21, 2012 282 283 ``````End: *)``````