begriffs open source - acsl-example/blob - proof/find3/interactive/lemma_Find_Limit.v

   1 (* This file is generated by Why3's Coq driver *)
   2 (* Beware! Only edit allowed sections below    *)
   3 Require Import BuiltIn.
   4 Require BuiltIn.
   5 Require HighOrd.
   6 Require bool.Bool.
   7 Require int.Int.
   8 Require int.Abs.
   9 Require int.ComputerDivision.
  10 Require real.Real.
  11 Require real.RealInfix.
  12 Require real.FromInt.
  13 Require map.Map.
  14
  15 Parameter eqb:
  16   forall {a:Type} {a_WT:WhyType a}, a -> a -> Init.Datatypes.bool.
  17
  18 Axiom eqb'def :
  19   forall {a:Type} {a_WT:WhyType a},
  20   forall (x:a) (y:a),
  21   ((x = y) -> ((eqb x y) = Init.Datatypes.true)) /\
  22   (~ (x = y) -> ((eqb x y) = Init.Datatypes.false)).
  23
  24 Parameter neqb:
  25   forall {a:Type} {a_WT:WhyType a}, a -> a -> Init.Datatypes.bool.
  26
  27 Axiom neqb'def :
  28   forall {a:Type} {a_WT:WhyType a},
  29   forall (x:a) (y:a),
  30   (~ (x = y) -> ((neqb x y) = Init.Datatypes.true)) /\
  31   ((x = y) -> ((neqb x y) = Init.Datatypes.false)).
  32
  33 Parameter zlt: Numbers.BinNums.Z -> Numbers.BinNums.Z -> Init.Datatypes.bool.
  34
  35 Axiom zlt'def :
  36   forall (x:Numbers.BinNums.Z) (y:Numbers.BinNums.Z),
  37   ((x < y)%Z -> ((zlt x y) = Init.Datatypes.true)) /\
  38   (~ (x < y)%Z -> ((zlt x y) = Init.Datatypes.false)).
  39
  40 Parameter zleq:
  41   Numbers.BinNums.Z -> Numbers.BinNums.Z -> Init.Datatypes.bool.
  42
  43 Axiom zleq'def :
  44   forall (x:Numbers.BinNums.Z) (y:Numbers.BinNums.Z),
  45   ((x <= y)%Z -> ((zleq x y) = Init.Datatypes.true)) /\
  46   (~ (x <= y)%Z -> ((zleq x y) = Init.Datatypes.false)).
  47
  48 Parameter rlt:
  49   Reals.Rdefinitions.R -> Reals.Rdefinitions.R -> Init.Datatypes.bool.
  50
  51 Axiom rlt'def :
  52   forall (x:Reals.Rdefinitions.R) (y:Reals.Rdefinitions.R),
  53   ((x < y)%R -> ((rlt x y) = Init.Datatypes.true)) /\
  54   (~ (x < y)%R -> ((rlt x y) = Init.Datatypes.false)).
  55
  56 Parameter rleq:
  57   Reals.Rdefinitions.R -> Reals.Rdefinitions.R -> Init.Datatypes.bool.
  58
  59 Axiom rleq'def :
  60   forall (x:Reals.Rdefinitions.R) (y:Reals.Rdefinitions.R),
  61   ((x <= y)%R -> ((rleq x y) = Init.Datatypes.true)) /\
  62   (~ (x <= y)%R -> ((rleq x y) = Init.Datatypes.false)).
  63
  64 (* Why3 assumption *)
  65 Definition real_of_int (x:Numbers.BinNums.Z) : Reals.Rdefinitions.R :=
  66   BuiltIn.IZR x.
  67
  68 Axiom c_euclidian :
  69   forall (n:Numbers.BinNums.Z) (d:Numbers.BinNums.Z), ~ (d = 0%Z) ->
  70   (n = (((ZArith.BinInt.Z.quot n d) * d)%Z + (ZArith.BinInt.Z.rem n d))%Z).
  71
  72 Axiom cmod_remainder :
  73   forall (n:Numbers.BinNums.Z) (d:Numbers.BinNums.Z),
  74   ((0%Z <= n)%Z -> (0%Z < d)%Z ->
  75    (0%Z <= (ZArith.BinInt.Z.rem n d))%Z /\ ((ZArith.BinInt.Z.rem n d) < d)%Z) /\
  76   ((n <= 0%Z)%Z -> (0%Z < d)%Z ->
  77    ((-d)%Z < (ZArith.BinInt.Z.rem n d))%Z /\
  78    ((ZArith.BinInt.Z.rem n d) <= 0%Z)%Z) /\
  79   ((0%Z <= n)%Z -> (d < 0%Z)%Z ->
  80    (0%Z <= (ZArith.BinInt.Z.rem n d))%Z /\
  81    ((ZArith.BinInt.Z.rem n d) < (-d)%Z)%Z) /\
  82   ((n <= 0%Z)%Z -> (d < 0%Z)%Z ->
  83    (d < (ZArith.BinInt.Z.rem n d))%Z /\ ((ZArith.BinInt.Z.rem n d) <= 0%Z)%Z).
  84
  85 Axiom cdiv_neutral :
  86   forall (a:Numbers.BinNums.Z), ((ZArith.BinInt.Z.quot a 1%Z) = a).
  87
  88 Axiom cdiv_inv :
  89   forall (a:Numbers.BinNums.Z), ~ (a = 0%Z) ->
  90   ((ZArith.BinInt.Z.quot a a) = 1%Z).
  91
  92 Axiom cdiv_closed_remainder :
  93   forall (a:Numbers.BinNums.Z) (b:Numbers.BinNums.Z) (n:Numbers.BinNums.Z),
  94   (0%Z <= a)%Z -> (0%Z <= b)%Z ->
  95   (0%Z <= (b - a)%Z)%Z /\ ((b - a)%Z < n)%Z ->
  96   ((ZArith.BinInt.Z.rem a n) = (ZArith.BinInt.Z.rem b n)) -> (a = b).
  97
  98 (* Why3 assumption *)
  99 Inductive addr :=
 100   | addr'mk : Numbers.BinNums.Z -> Numbers.BinNums.Z -> addr.
 101 Axiom addr_WhyType : WhyType addr.
 102 Existing Instance addr_WhyType.
 103
 104 (* Why3 assumption *)
 105 Definition base (v:addr) : Numbers.BinNums.Z :=
 106   match v with
 107   | addr'mk x x1 => x
 108   end.
 109
 110 (* Why3 assumption *)
 111 Definition offset (v:addr) : Numbers.BinNums.Z :=
 112   match v with
 113   | addr'mk x x1 => x1
 114   end.
 115
 116 (* Why3 assumption *)
 117 Definition malloc := Numbers.BinNums.Z -> Numbers.BinNums.Z.
 118
 119 (* Why3 assumption *)
 120 Definition null : addr := addr'mk 0%Z 0%Z.
 121
 122 (* Why3 assumption *)
 123 Definition global (b:Numbers.BinNums.Z) : addr := addr'mk b 0%Z.
 124
 125 Parameter addr_le: addr -> addr -> Prop.
 126
 127 Parameter addr_lt: addr -> addr -> Prop.
 128
 129 Parameter addr_le_bool: addr -> addr -> Init.Datatypes.bool.
 130
 131 Parameter addr_lt_bool: addr -> addr -> Init.Datatypes.bool.
 132
 133 Axiom addr_le_def :
 134   forall (p:addr) (q:addr), ((base p) = (base q)) ->
 135   addr_le p q <-> ((offset p) <= (offset q))%Z.
 136
 137 Axiom addr_lt_def :
 138   forall (p:addr) (q:addr), ((base p) = (base q)) ->
 139   addr_lt p q <-> ((offset p) < (offset q))%Z.
 140
 141 Axiom addr_le_bool_def :
 142   forall (p:addr) (q:addr),
 143   addr_le p q <-> ((addr_le_bool p q) = Init.Datatypes.true).
 144
 145 Axiom addr_lt_bool_def :
 146   forall (p:addr) (q:addr),
 147   addr_lt p q <-> ((addr_lt_bool p q) = Init.Datatypes.true).
 148
 149 (* Why3 assumption *)
 150 Definition shift (p:addr) (k:Numbers.BinNums.Z) : addr :=
 151   addr'mk (base p) ((offset p) + k)%Z.
 152
 153 (* Why3 assumption *)
 154 Definition valid_rw (m:Numbers.BinNums.Z -> Numbers.BinNums.Z) (p:addr)
 155     (n:Numbers.BinNums.Z) : Prop :=
 156   (0%Z < n)%Z ->
 157   (0%Z < (base p))%Z /\
 158   (0%Z <= (offset p))%Z /\ (((offset p) + n)%Z <= (m (base p)))%Z.
 159
 160 (* Why3 assumption *)
 161 Definition valid_rd (m:Numbers.BinNums.Z -> Numbers.BinNums.Z) (p:addr)
 162     (n:Numbers.BinNums.Z) : Prop :=
 163   (0%Z < n)%Z ->
 164   ~ (0%Z = (base p)) /\
 165   (0%Z <= (offset p))%Z /\ (((offset p) + n)%Z <= (m (base p)))%Z.
 166
 167 (* Why3 assumption *)
 168 Definition valid_obj (m:Numbers.BinNums.Z -> Numbers.BinNums.Z) (p:addr) :
 169     Prop :=
 170   ~ (0%Z = (base p)) /\
 171   (0%Z <= (offset p))%Z /\
 172   ((offset p) <= (m (base p)))%Z /\ (0%Z < (m (base p)))%Z.
 173
 174 (* Why3 assumption *)
 175 Definition invalid (m:Numbers.BinNums.Z -> Numbers.BinNums.Z) (p:addr)
 176     (n:Numbers.BinNums.Z) : Prop :=
 177   (n <= 0%Z)%Z \/
 178   ((base p) = 0%Z) \/
 179   ((m (base p)) <= (offset p))%Z \/ (((offset p) + n)%Z <= 0%Z)%Z.
 180
 181 Axiom valid_rw_rd :
 182   forall (m:Numbers.BinNums.Z -> Numbers.BinNums.Z), forall (p:addr),
 183   forall (n:Numbers.BinNums.Z), valid_rw m p n -> valid_rd m p n.
 184
 185 Axiom valid_string :
 186   forall (m:Numbers.BinNums.Z -> Numbers.BinNums.Z), forall (p:addr),
 187   ((base p) < 0%Z)%Z ->
 188   (0%Z <= (offset p))%Z /\ ((offset p) < (m (base p)))%Z ->
 189   valid_rd m p 1%Z /\ ~ valid_rw m p 1%Z.
 190
 191 (* Why3 assumption *)
 192 Definition included (p:addr) (lp:Numbers.BinNums.Z) (q:addr)
 193     (lq:Numbers.BinNums.Z) : Prop :=
 194   (0%Z < lp)%Z ->
 195   (0%Z <= lq)%Z /\
 196   ((base p) = (base q)) /\
 197   ((offset q) <= (offset p))%Z /\
 198   (((offset p) + lp)%Z <= ((offset q) + lq)%Z)%Z.
 199
 200 (* Why3 assumption *)
 201 Definition separated (p:addr) (lp:Numbers.BinNums.Z) (q:addr)
 202     (lq:Numbers.BinNums.Z) : Prop :=
 203   (lp <= 0%Z)%Z \/
 204   (lq <= 0%Z)%Z \/
 205   ~ ((base p) = (base q)) \/
 206   (((offset q) + lq)%Z <= (offset p))%Z \/
 207   (((offset p) + lp)%Z <= (offset q))%Z.
 208
 209 Axiom separated_1 :
 210   forall (p:addr) (q:addr),
 211   forall (lp:Numbers.BinNums.Z) (lq:Numbers.BinNums.Z) (i:Numbers.BinNums.Z)
 212     (j:Numbers.BinNums.Z),
 213   separated p lp q lq ->
 214   ((offset p) <= i)%Z /\ (i < ((offset p) + lp)%Z)%Z ->
 215   ((offset q) <= j)%Z /\ (j < ((offset q) + lq)%Z)%Z ->
 216   ~ ((addr'mk (base p) i) = (addr'mk (base q) j)).
 217
 218 Axiom separated_included :
 219   forall (p:addr) (q:addr),
 220   forall (lp:Numbers.BinNums.Z) (lq:Numbers.BinNums.Z), (0%Z < lp)%Z ->
 221   (0%Z < lq)%Z -> separated p lp q lq -> ~ included p lp q lq.
 222
 223 Axiom included_trans :
 224   forall (p:addr) (q:addr) (r:addr),
 225   forall (lp:Numbers.BinNums.Z) (lq:Numbers.BinNums.Z) (lr:Numbers.BinNums.Z),
 226   included p lp q lq -> included q lq r lr -> included p lp r lr.
 227
 228 Axiom separated_trans :
 229   forall (p:addr) (q:addr) (r:addr),
 230   forall (lp:Numbers.BinNums.Z) (lq:Numbers.BinNums.Z) (lr:Numbers.BinNums.Z),
 231   included p lp q lq -> separated q lq r lr -> separated p lp r lr.
 232
 233 Axiom separated_sym :
 234   forall (p:addr) (q:addr),
 235   forall (lp:Numbers.BinNums.Z) (lq:Numbers.BinNums.Z),
 236   separated p lp q lq <-> separated q lq p lp.
 237
 238 Parameter binit: Numbers.BinNums.Z -> Prop.
 239
 240 Parameter region: Numbers.BinNums.Z -> Numbers.BinNums.Z.
 241
 242 Parameter linked: (Numbers.BinNums.Z -> Numbers.BinNums.Z) -> Prop.
 243
 244 Parameter static_malloc: Numbers.BinNums.Z -> Numbers.BinNums.Z.
 245
 246 (* Why3 assumption *)
 247 Definition statically_allocated (base1:Numbers.BinNums.Z) : Prop :=
 248   (base1 = 0%Z) \/ (0%Z < (static_malloc base1))%Z.
 249
 250 Axiom valid_pointers_are_statically_allocated :
 251   forall (a:addr) (m:Numbers.BinNums.Z -> Numbers.BinNums.Z)
 252     (n:Numbers.BinNums.Z),
 253   (0%Z < n)%Z -> valid_rd m a n -> statically_allocated (base a).
 254
 255 Parameter int_of_addr: addr -> Numbers.BinNums.Z.
 256
 257 Parameter addr_of_int: Numbers.BinNums.Z -> addr.
 258
 259 Axiom addr_of_null : ((int_of_addr null) = 0%Z).
 260
 261 Axiom addr_of_int_bijection :
 262   forall (p:addr), statically_allocated (base p) ->
 263   ((addr_of_int (int_of_addr p)) = p).
 264
 265 Axiom table : Type.
 266 Parameter table_WhyType : WhyType table.
 267 Existing Instance table_WhyType.
 268
 269 Parameter table_of_base: Numbers.BinNums.Z -> table.
 270
 271 Parameter table_to_offset: table -> Numbers.BinNums.Z -> Numbers.BinNums.Z.
 272
 273 Axiom table_to_offset_zero :
 274   forall (t:table), ((table_to_offset t 0%Z) = 0%Z).
 275
 276 Axiom table_to_offset_monotonic :
 277   forall (t:table), forall (o1:Numbers.BinNums.Z) (o2:Numbers.BinNums.Z),
 278   (o1 <= o2)%Z <-> ((table_to_offset t o1) <= (table_to_offset t o2))%Z.
 279
 280 Parameter L_Find_1_:
 281   (addr -> Numbers.BinNums.Z) -> addr -> Numbers.BinNums.Z ->
 282   Numbers.BinNums.Z -> Numbers.BinNums.Z -> Numbers.BinNums.Z.
 283
 284 Axiom L_Find_1__def :
 285   forall (Mint:addr -> Numbers.BinNums.Z) (a:addr) (m:Numbers.BinNums.Z)
 286     (n:Numbers.BinNums.Z) (v:Numbers.BinNums.Z),
 287   let x := ((-1%Z)%Z + n)%Z in
 288   let x1 := L_Find_1_ Mint a m x v in
 289   let x2 := ((-1%Z)%Z * m)%Z in
 290   ((n <= m)%Z -> ((L_Find_1_ Mint a m n v) = 0%Z)) /\
 291   (~ (n <= m)%Z ->
 292    ((0%Z <= x1)%Z /\ (((2%Z + m)%Z + x1)%Z <= n)%Z ->
 293     ((L_Find_1_ Mint a m n v) = x1)) /\
 294    (~ ((0%Z <= x1)%Z /\ (((2%Z + m)%Z + x1)%Z <= n)%Z) ->
 295     (((Mint (shift a x)) = v) ->
 296      ((L_Find_1_ Mint a m n v) = (((-1%Z)%Z + n)%Z + x2)%Z)) /\
 297     (~ ((Mint (shift a x)) = v) -> ((L_Find_1_ Mint a m n v) = (n + x2)%Z)))).
 298
 299 (* Why3 assumption *)
 300 Definition is_bool (x:Numbers.BinNums.Z) : Prop := (x = 0%Z) \/ (x = 1%Z).
 301
 302 (* Why3 assumption *)
 303 Definition is_uint8 (x:Numbers.BinNums.Z) : Prop :=
 304   (0%Z <= x)%Z /\ (x < 256%Z)%Z.
 305
 306 (* Why3 assumption *)
 307 Definition is_sint8 (x:Numbers.BinNums.Z) : Prop :=
 308   ((-128%Z)%Z <= x)%Z /\ (x < 128%Z)%Z.
 309
 310 (* Why3 assumption *)
 311 Definition is_uint16 (x:Numbers.BinNums.Z) : Prop :=
 312   (0%Z <= x)%Z /\ (x < 65536%Z)%Z.
 313
 314 (* Why3 assumption *)
 315 Definition is_sint16 (x:Numbers.BinNums.Z) : Prop :=
 316   ((-32768%Z)%Z <= x)%Z /\ (x < 32768%Z)%Z.
 317
 318 (* Why3 assumption *)
 319 Definition is_uint32 (x:Numbers.BinNums.Z) : Prop :=
 320   (0%Z <= x)%Z /\ (x < 4294967296%Z)%Z.
 321
 322 (* Why3 assumption *)
 323 Definition is_sint32 (x:Numbers.BinNums.Z) : Prop :=
 324   ((-2147483648%Z)%Z <= x)%Z /\ (x < 2147483648%Z)%Z.
 325
 326 (* Why3 assumption *)
 327 Definition is_uint64 (x:Numbers.BinNums.Z) : Prop :=
 328   (0%Z <= x)%Z /\ (x < 18446744073709551616%Z)%Z.
 329
 330 (* Why3 assumption *)
 331 Definition is_sint64 (x:Numbers.BinNums.Z) : Prop :=
 332   ((-9223372036854775808%Z)%Z <= x)%Z /\ (x < 9223372036854775808%Z)%Z.
 333
 334 Axiom is_bool0 : is_bool 0%Z.
 335
 336 Axiom is_bool1 : is_bool 1%Z.
 337
 338 Parameter to_bool: Numbers.BinNums.Z -> Numbers.BinNums.Z.
 339
 340 Axiom to_bool'def :
 341   forall (x:Numbers.BinNums.Z),
 342   ((x = 0%Z) -> ((to_bool x) = 0%Z)) /\ (~ (x = 0%Z) -> ((to_bool x) = 1%Z)).
 343
 344 Parameter to_uint8: Numbers.BinNums.Z -> Numbers.BinNums.Z.
 345
 346 Axiom to_uint8'def :
 347   forall (x:Numbers.BinNums.Z),
 348   ((x < 0%Z)%Z -> ((to_uint8 x) = (to_uint8 (x + 256%Z)%Z))) /\
 349   (~ (x < 0%Z)%Z ->
 350    ((256%Z <= x)%Z -> ((to_uint8 x) = (to_uint8 (x - 256%Z)%Z))) /\
 351    (~ (256%Z <= x)%Z -> ((to_uint8 x) = x))).
 352
 353 Parameter to_sint8: Numbers.BinNums.Z -> Numbers.BinNums.Z.
 354
 355 Axiom to_sint8'def :
 356   forall (x:Numbers.BinNums.Z),
 357   ((x < (-128%Z)%Z)%Z -> ((to_sint8 x) = (to_sint8 (x + 256%Z)%Z))) /\
 358   (~ (x < (-128%Z)%Z)%Z ->
 359    ((128%Z <= x)%Z -> ((to_sint8 x) = (to_sint8 (x - 256%Z)%Z))) /\
 360    (~ (128%Z <= x)%Z -> ((to_sint8 x) = x))).
 361
 362 Parameter to_uint16: Numbers.BinNums.Z -> Numbers.BinNums.Z.
 363
 364 Axiom to_uint16'def :
 365   forall (x:Numbers.BinNums.Z),
 366   ((x < 0%Z)%Z -> ((to_uint16 x) = (to_uint16 (x + 65536%Z)%Z))) /\
 367   (~ (x < 0%Z)%Z ->
 368    ((65536%Z <= x)%Z -> ((to_uint16 x) = (to_uint16 (x - 65536%Z)%Z))) /\
 369    (~ (65536%Z <= x)%Z -> ((to_uint16 x) = x))).
 370
 371 Parameter to_sint16: Numbers.BinNums.Z -> Numbers.BinNums.Z.
 372
 373 Axiom to_sint16'def :
 374   forall (x:Numbers.BinNums.Z),
 375   ((x < (-32768%Z)%Z)%Z -> ((to_sint16 x) = (to_sint16 (x + 65536%Z)%Z))) /\
 376   (~ (x < (-32768%Z)%Z)%Z ->
 377    ((32768%Z <= x)%Z -> ((to_sint16 x) = (to_sint16 (x - 65536%Z)%Z))) /\
 378    (~ (32768%Z <= x)%Z -> ((to_sint16 x) = x))).
 379
 380 Parameter to_uint32: Numbers.BinNums.Z -> Numbers.BinNums.Z.
 381
 382 Axiom to_uint32'def :
 383   forall (x:Numbers.BinNums.Z),
 384   ((x < 0%Z)%Z -> ((to_uint32 x) = (to_uint32 (x + 4294967296%Z)%Z))) /\
 385   (~ (x < 0%Z)%Z ->
 386    ((4294967296%Z <= x)%Z ->
 387     ((to_uint32 x) = (to_uint32 (x - 4294967296%Z)%Z))) /\
 388    (~ (4294967296%Z <= x)%Z -> ((to_uint32 x) = x))).
 389
 390 Parameter to_sint32: Numbers.BinNums.Z -> Numbers.BinNums.Z.
 391
 392 Axiom to_sint32'def :
 393   forall (x:Numbers.BinNums.Z),
 394   ((x < (-2147483648%Z)%Z)%Z ->
 395    ((to_sint32 x) = (to_sint32 (x + 4294967296%Z)%Z))) /\
 396   (~ (x < (-2147483648%Z)%Z)%Z ->
 397    ((2147483648%Z <= x)%Z ->
 398     ((to_sint32 x) = (to_sint32 (x - 4294967296%Z)%Z))) /\
 399    (~ (2147483648%Z <= x)%Z -> ((to_sint32 x) = x))).
 400
 401 Parameter to_uint64: Numbers.BinNums.Z -> Numbers.BinNums.Z.
 402
 403 Axiom to_uint64'def :
 404   forall (x:Numbers.BinNums.Z),
 405   ((x < 0%Z)%Z ->
 406    ((to_uint64 x) = (to_uint64 (x + 18446744073709551616%Z)%Z))) /\
 407   (~ (x < 0%Z)%Z ->
 408    ((18446744073709551616%Z <= x)%Z ->
 409     ((to_uint64 x) = (to_uint64 (x - 18446744073709551616%Z)%Z))) /\
 410    (~ (18446744073709551616%Z <= x)%Z -> ((to_uint64 x) = x))).
 411
 412 Parameter to_sint64: Numbers.BinNums.Z -> Numbers.BinNums.Z.
 413
 414 Axiom to_sint64'def :
 415   forall (x:Numbers.BinNums.Z),
 416   ((x < (-9223372036854775808%Z)%Z)%Z ->
 417    ((to_sint64 x) = (to_sint64 (x + 18446744073709551616%Z)%Z))) /\
 418   (~ (x < (-9223372036854775808%Z)%Z)%Z ->
 419    ((9223372036854775808%Z <= x)%Z ->
 420     ((to_sint64 x) = (to_sint64 (x - 18446744073709551616%Z)%Z))) /\
 421    (~ (9223372036854775808%Z <= x)%Z -> ((to_sint64 x) = x))).
 422
 423 Parameter two_power_abs: Numbers.BinNums.Z -> Numbers.BinNums.Z.
 424
 425 (* Why3 assumption *)
 426 Definition is_uint (n:Numbers.BinNums.Z) (x:Numbers.BinNums.Z) : Prop :=
 427   (0%Z <= x)%Z /\ (x < (two_power_abs n))%Z.
 428
 429 (* Why3 assumption *)
 430 Definition is_sint (n:Numbers.BinNums.Z) (x:Numbers.BinNums.Z) : Prop :=
 431   ((-(two_power_abs n))%Z <= x)%Z /\ (x < (two_power_abs n))%Z.
 432
 433 Parameter to_uint:
 434   Numbers.BinNums.Z -> Numbers.BinNums.Z -> Numbers.BinNums.Z.
 435
 436 Parameter to_sint:
 437   Numbers.BinNums.Z -> Numbers.BinNums.Z -> Numbers.BinNums.Z.
 438
 439 Axiom is_to_uint8 : forall (x:Numbers.BinNums.Z), is_uint8 (to_uint8 x).
 440
 441 Axiom is_to_sint8 : forall (x:Numbers.BinNums.Z), is_sint8 (to_sint8 x).
 442
 443 Axiom is_to_uint16 : forall (x:Numbers.BinNums.Z), is_uint16 (to_uint16 x).
 444
 445 Axiom is_to_sint16 : forall (x:Numbers.BinNums.Z), is_sint16 (to_sint16 x).
 446
 447 Axiom is_to_uint32 : forall (x:Numbers.BinNums.Z), is_uint32 (to_uint32 x).
 448
 449 Axiom is_to_sint32 : forall (x:Numbers.BinNums.Z), is_sint32 (to_sint32 x).
 450
 451 Axiom is_to_uint64 : forall (x:Numbers.BinNums.Z), is_uint64 (to_uint64 x).
 452
 453 Axiom is_to_sint64 : forall (x:Numbers.BinNums.Z), is_sint64 (to_sint64 x).
 454
 455 Axiom id_uint8 :
 456   forall (x:Numbers.BinNums.Z), is_uint8 x -> ((to_uint8 x) = x).
 457
 458 Axiom id_sint8 :
 459   forall (x:Numbers.BinNums.Z), is_sint8 x -> ((to_sint8 x) = x).
 460
 461 Axiom id_uint16 :
 462   forall (x:Numbers.BinNums.Z), is_uint16 x -> ((to_uint16 x) = x).
 463
 464 Axiom id_sint16 :
 465   forall (x:Numbers.BinNums.Z), is_sint16 x -> ((to_sint16 x) = x).
 466
 467 Axiom id_uint32 :
 468   forall (x:Numbers.BinNums.Z), is_uint32 x -> ((to_uint32 x) = x).
 469
 470 Axiom id_sint32 :
 471   forall (x:Numbers.BinNums.Z), is_sint32 x -> ((to_sint32 x) = x).
 472
 473 Axiom id_uint64 :
 474   forall (x:Numbers.BinNums.Z), is_uint64 x -> ((to_uint64 x) = x).
 475
 476 Axiom id_sint64 :
 477   forall (x:Numbers.BinNums.Z), is_sint64 x -> ((to_sint64 x) = x).
 478
 479 Axiom id_uint8_inl :
 480   forall (x:Numbers.BinNums.Z), (0%Z <= x)%Z /\ (x < 256%Z)%Z ->
 481   ((to_uint8 x) = x).
 482
 483 Axiom id_sint8_inl :
 484   forall (x:Numbers.BinNums.Z), ((-128%Z)%Z <= x)%Z /\ (x < 128%Z)%Z ->
 485   ((to_sint8 x) = x).
 486
 487 Axiom id_uint16_inl :
 488   forall (x:Numbers.BinNums.Z), (0%Z <= x)%Z /\ (x < 65536%Z)%Z ->
 489   ((to_uint16 x) = x).
 490
 491 Axiom id_sint16_inl :
 492   forall (x:Numbers.BinNums.Z), ((-32768%Z)%Z <= x)%Z /\ (x < 32768%Z)%Z ->
 493   ((to_sint16 x) = x).
 494
 495 Axiom id_uint32_inl :
 496   forall (x:Numbers.BinNums.Z), (0%Z <= x)%Z /\ (x < 4294967296%Z)%Z ->
 497   ((to_uint32 x) = x).
 498
 499 Axiom id_sint32_inl :
 500   forall (x:Numbers.BinNums.Z),
 501   ((-2147483648%Z)%Z <= x)%Z /\ (x < 2147483648%Z)%Z -> ((to_sint32 x) = x).
 502
 503 Axiom id_uint64_inl :
 504   forall (x:Numbers.BinNums.Z),
 505   (0%Z <= x)%Z /\ (x < 18446744073709551616%Z)%Z -> ((to_uint64 x) = x).
 506
 507 Axiom id_sint64_inl :
 508   forall (x:Numbers.BinNums.Z),
 509   ((-9223372036854775808%Z)%Z <= x)%Z /\ (x < 9223372036854775808%Z)%Z ->
 510   ((to_sint64 x) = x).
 511
 512 Axiom proj_int8 :
 513   forall (x:Numbers.BinNums.Z), ((to_sint8 (to_uint8 x)) = (to_sint8 x)).
 514
 515 Axiom proj_int16 :
 516   forall (x:Numbers.BinNums.Z), ((to_sint16 (to_uint16 x)) = (to_sint16 x)).
 517
 518 Axiom proj_int32 :
 519   forall (x:Numbers.BinNums.Z), ((to_sint32 (to_uint32 x)) = (to_sint32 x)).
 520
 521 Axiom proj_int64 :
 522   forall (x:Numbers.BinNums.Z), ((to_sint64 (to_uint64 x)) = (to_sint64 x)).
 523
 524 Axiom Q_Find_Extend :
 525   forall (Mint:addr -> Numbers.BinNums.Z) (a:addr) (v:Numbers.BinNums.Z)
 526     (k:Numbers.BinNums.Z) (m:Numbers.BinNums.Z) (n:Numbers.BinNums.Z),
 527   let x := Mint (shift a k) in
 528   (x = v) -> ((m + (L_Find_1_ Mint a m k v))%Z = k) -> (m <= k)%Z ->
 529   (k < n)%Z -> is_sint32 v -> is_sint32 x ->
 530   ((m + (L_Find_1_ Mint a m n v))%Z = k).
 531
 532 Axiom Q_Find_Increasing :
 533   forall (Mint:addr -> Numbers.BinNums.Z) (a:addr) (v:Numbers.BinNums.Z)
 534     (k:Numbers.BinNums.Z) (m:Numbers.BinNums.Z) (n:Numbers.BinNums.Z),
 535   (m <= k)%Z -> (k <= n)%Z -> is_sint32 v ->
 536   ((L_Find_1_ Mint a m k v) <= (L_Find_1_ Mint a m n v))%Z.
 537
 538 Axiom Q_Find_WeaklyIncreasing :
 539   forall (Mint:addr -> Numbers.BinNums.Z) (a:addr) (v:Numbers.BinNums.Z)
 540     (m:Numbers.BinNums.Z) (n:Numbers.BinNums.Z),
 541   (m <= n)%Z -> is_sint32 v ->
 542   ((L_Find_1_ Mint a m n v) <= (L_Find_1_ Mint a m (1%Z + n)%Z v))%Z.
 543
 544 Axiom Q_Find_Upper :
 545   forall (Mint:addr -> Numbers.BinNums.Z) (a:addr) (v:Numbers.BinNums.Z)
 546     (m:Numbers.BinNums.Z) (n:Numbers.BinNums.Z),
 547   (m <= n)%Z -> is_sint32 v -> ((m + (L_Find_1_ Mint a m n v))%Z <= n)%Z.
 548
 549 Axiom Q_Find_Lower :
 550   forall (Mint:addr -> Numbers.BinNums.Z) (a:addr) (v:Numbers.BinNums.Z)
 551     (m:Numbers.BinNums.Z) (n:Numbers.BinNums.Z),
 552   is_sint32 v -> (0%Z <= (L_Find_1_ Mint a m n v))%Z.
 553
 554 Axiom Q_Find_MissMiss :
 555   forall (Mint:addr -> Numbers.BinNums.Z) (a:addr) (v:Numbers.BinNums.Z)
 556     (m:Numbers.BinNums.Z) (n:Numbers.BinNums.Z),
 557   let x := Mint (shift a n) in
 558   let x1 := (1%Z + n)%Z in
 559   ~ (x = v) -> ((m + (L_Find_1_ Mint a m n v))%Z = n) -> (m <= n)%Z ->
 560   is_sint32 v -> is_sint32 x -> ((m + (L_Find_1_ Mint a m x1 v))%Z = x1).
 561
 562 Axiom Q_Find_MissHit :
 563   forall (Mint:addr -> Numbers.BinNums.Z) (a:addr) (v:Numbers.BinNums.Z)
 564     (m:Numbers.BinNums.Z) (n:Numbers.BinNums.Z),
 565   let x := Mint (shift a n) in
 566   (x = v) -> ((m + (L_Find_1_ Mint a m n v))%Z = n) -> (m <= n)%Z ->
 567   is_sint32 v -> is_sint32 x ->
 568   ((m + (L_Find_1_ Mint a m (1%Z + n)%Z v))%Z = n).
 569
 570 Axiom Q_Find_Hit :
 571   forall (Mint:addr -> Numbers.BinNums.Z) (a:addr) (v:Numbers.BinNums.Z)
 572     (m:Numbers.BinNums.Z) (n:Numbers.BinNums.Z),
 573   let x := L_Find_1_ Mint a m n v in
 574   (m <= n)%Z -> ((m + x)%Z < n)%Z -> is_sint32 v ->
 575   ((L_Find_1_ Mint a m (1%Z + n)%Z v) = x).
 576
 577 Axiom Q_Find_Empty :
 578   forall (Mint:addr -> Numbers.BinNums.Z) (a:addr) (v:Numbers.BinNums.Z)
 579     (m:Numbers.BinNums.Z) (n:Numbers.BinNums.Z),
 580   (n <= m)%Z -> is_sint32 v -> ((L_Find_1_ Mint a m n v) = 0%Z).
 581
 582 (* Why3 goal *)
 583 Theorem wp_goal :
 584   forall (t:addr -> Numbers.BinNums.Z) (a:addr) (i:Numbers.BinNums.Z)
 585     (i1:Numbers.BinNums.Z) (i2:Numbers.BinNums.Z),
 586   let x := t (shift a i) in
 587   (i < i2)%Z -> (i1 <= i)%Z -> is_sint32 x ->
 588   ((i1 + (L_Find_1_ t a i1 i2 x))%Z <= i)%Z.
 589 Proof.
 590 intros t a i i1 i2 x h1 h2 h3.
 591
 592 Qed.
 593