double_of_int.why 10.6 KB
Newer Older
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

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

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

124
  lemma from_int2c_to_nat_sub_pos:
Andrei Paskevich's avatar
Andrei Paskevich committed
125 126
  	forall i:int. 0 <= i <= 31 ->
          forall x:int. 0 <= x <  Pow2int.pow2 i ->
127 128
           BV32.to_nat_sub (BV32.from_int2c x) (i-1) 0 = x

Andrei Paskevich's avatar
Andrei Paskevich committed
129
  lemma lemma1_pos : forall x:int. is_int32 x /\ x >= 0 ->
130 131 132 133
  	BV32.to_nat_sub (jpxor x) 31 0 = Pow2int.pow2 31 + x

  (* case x < 0 *)

Andrei Paskevich's avatar
Andrei Paskevich committed
134
  lemma jpxorx_neg: forall x:int. x<0 ->
135 136 137
  	BV32.nth (BV32.bw_xor j' (BV32.from_int2c x)) 31 = False

  lemma from_int2c_to_nat_sub_neg:
Andrei Paskevich's avatar
Andrei Paskevich committed
138 139
  	forall i:int. 0 <= i <= 31 ->
          forall x:int. -Pow2int.pow2 i <= x <  0 ->
140
           BV32.to_nat_sub (BV32.from_int2c x) (i-1) 0 = Pow2int.pow2 i + x
Andrei Paskevich's avatar
Andrei Paskevich committed
141 142

  lemma lemma1_neg : forall x:int. is_int32 x /\ x < 0 ->
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

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's avatar
Andrei Paskevich committed
157 158
  	forall i:int. 0 <= i <= 30 ->
          forall x:int. 0 <= x <  Pow2int.pow2 i ->
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

176
****)
177

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
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's avatar
Andrei Paskevich committed
192

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)

198 199
  lemma nth_var3: forall x i:int. 
    is_int32 x /\ 32 <= i <= 51 -> BV64.nth (var x) i = False
Andrei Paskevich's avatar
Andrei Paskevich committed
200

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                   *)
  (*********************************************************************)

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
215

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
224 225 226 227 228

  (*********************************************************************)
  (*  lemma 4: for all integer x, sign(var(x)) = false                 *)
  (*********************************************************************)

229 230
  lemma nth_var9: 
    forall x:int. is_int32 x -> BV64.nth (var x) 63 = False
231

232 233
  lemma lemma4 : 
    forall x:int. is_int32 x -> sign(var(x)) = False
234 235 236 237

  (*********************************************************************)
  (*  lemma 5: for all integer x, var_as_double(x) = 2^52 + 2^31 + x   *)
  (*********************************************************************)
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))
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:
281
compile-command: "why3 ide -L . double_of_int.why"
282 283
End:
*)