begriffs open source - acsl-example/blob - proof/find3/interactive/lemma_Find_ResultEqual.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 (* Why3 assumption *)
 281 Definition is_bool (x:Numbers.BinNums.Z) : Prop := (x = 0%Z) \/ (x = 1%Z).
 282
 283 (* Why3 assumption *)
 284 Definition is_uint8 (x:Numbers.BinNums.Z) : Prop :=
 285   (0%Z <= x)%Z /\ (x < 256%Z)%Z.
 286
 287 (* Why3 assumption *)
 288 Definition is_sint8 (x:Numbers.BinNums.Z) : Prop :=
 289   ((-128%Z)%Z <= x)%Z /\ (x < 128%Z)%Z.
 290
 291 (* Why3 assumption *)
 292 Definition is_uint16 (x:Numbers.BinNums.Z) : Prop :=
 293   (0%Z <= x)%Z /\ (x < 65536%Z)%Z.
 294
 295 (* Why3 assumption *)
 296 Definition is_sint16 (x:Numbers.BinNums.Z) : Prop :=
 297   ((-32768%Z)%Z <= x)%Z /\ (x < 32768%Z)%Z.
 298
 299 (* Why3 assumption *)
 300 Definition is_uint32 (x:Numbers.BinNums.Z) : Prop :=
 301   (0%Z <= x)%Z /\ (x < 4294967296%Z)%Z.
 302
 303 (* Why3 assumption *)
 304 Definition is_sint32 (x:Numbers.BinNums.Z) : Prop :=
 305   ((-2147483648%Z)%Z <= x)%Z /\ (x < 2147483648%Z)%Z.
 306
 307 (* Why3 assumption *)
 308 Definition is_uint64 (x:Numbers.BinNums.Z) : Prop :=
 309   (0%Z <= x)%Z /\ (x < 18446744073709551616%Z)%Z.
 310
 311 (* Why3 assumption *)
 312 Definition is_sint64 (x:Numbers.BinNums.Z) : Prop :=
 313   ((-9223372036854775808%Z)%Z <= x)%Z /\ (x < 9223372036854775808%Z)%Z.
 314
 315 Axiom is_bool0 : is_bool 0%Z.
 316
 317 Axiom is_bool1 : is_bool 1%Z.
 318
 319 Parameter to_bool: Numbers.BinNums.Z -> Numbers.BinNums.Z.
 320
 321 Axiom to_bool'def :
 322   forall (x:Numbers.BinNums.Z),
 323   ((x = 0%Z) -> ((to_bool x) = 0%Z)) /\ (~ (x = 0%Z) -> ((to_bool x) = 1%Z)).
 324
 325 Parameter to_uint8: Numbers.BinNums.Z -> Numbers.BinNums.Z.
 326
 327 Axiom to_uint8'def :
 328   forall (x:Numbers.BinNums.Z),
 329   ((x < 0%Z)%Z -> ((to_uint8 x) = (to_uint8 (x + 256%Z)%Z))) /\
 330   (~ (x < 0%Z)%Z ->
 331    ((256%Z <= x)%Z -> ((to_uint8 x) = (to_uint8 (x - 256%Z)%Z))) /\
 332    (~ (256%Z <= x)%Z -> ((to_uint8 x) = x))).
 333
 334 Parameter to_sint8: Numbers.BinNums.Z -> Numbers.BinNums.Z.
 335
 336 Axiom to_sint8'def :
 337   forall (x:Numbers.BinNums.Z),
 338   ((x < (-128%Z)%Z)%Z -> ((to_sint8 x) = (to_sint8 (x + 256%Z)%Z))) /\
 339   (~ (x < (-128%Z)%Z)%Z ->
 340    ((128%Z <= x)%Z -> ((to_sint8 x) = (to_sint8 (x - 256%Z)%Z))) /\
 341    (~ (128%Z <= x)%Z -> ((to_sint8 x) = x))).
 342
 343 Parameter to_uint16: Numbers.BinNums.Z -> Numbers.BinNums.Z.
 344
 345 Axiom to_uint16'def :
 346   forall (x:Numbers.BinNums.Z),
 347   ((x < 0%Z)%Z -> ((to_uint16 x) = (to_uint16 (x + 65536%Z)%Z))) /\
 348   (~ (x < 0%Z)%Z ->
 349    ((65536%Z <= x)%Z -> ((to_uint16 x) = (to_uint16 (x - 65536%Z)%Z))) /\
 350    (~ (65536%Z <= x)%Z -> ((to_uint16 x) = x))).
 351
 352 Parameter to_sint16: Numbers.BinNums.Z -> Numbers.BinNums.Z.
 353
 354 Axiom to_sint16'def :
 355   forall (x:Numbers.BinNums.Z),
 356   ((x < (-32768%Z)%Z)%Z -> ((to_sint16 x) = (to_sint16 (x + 65536%Z)%Z))) /\
 357   (~ (x < (-32768%Z)%Z)%Z ->
 358    ((32768%Z <= x)%Z -> ((to_sint16 x) = (to_sint16 (x - 65536%Z)%Z))) /\
 359    (~ (32768%Z <= x)%Z -> ((to_sint16 x) = x))).
 360
 361 Parameter to_uint32: Numbers.BinNums.Z -> Numbers.BinNums.Z.
 362
 363 Axiom to_uint32'def :
 364   forall (x:Numbers.BinNums.Z),
 365   ((x < 0%Z)%Z -> ((to_uint32 x) = (to_uint32 (x + 4294967296%Z)%Z))) /\
 366   (~ (x < 0%Z)%Z ->
 367    ((4294967296%Z <= x)%Z ->
 368     ((to_uint32 x) = (to_uint32 (x - 4294967296%Z)%Z))) /\
 369    (~ (4294967296%Z <= x)%Z -> ((to_uint32 x) = x))).
 370
 371 Parameter to_sint32: Numbers.BinNums.Z -> Numbers.BinNums.Z.
 372
 373 Axiom to_sint32'def :
 374   forall (x:Numbers.BinNums.Z),
 375   ((x < (-2147483648%Z)%Z)%Z ->
 376    ((to_sint32 x) = (to_sint32 (x + 4294967296%Z)%Z))) /\
 377   (~ (x < (-2147483648%Z)%Z)%Z ->
 378    ((2147483648%Z <= x)%Z ->
 379     ((to_sint32 x) = (to_sint32 (x - 4294967296%Z)%Z))) /\
 380    (~ (2147483648%Z <= x)%Z -> ((to_sint32 x) = x))).
 381
 382 Parameter to_uint64: Numbers.BinNums.Z -> Numbers.BinNums.Z.
 383
 384 Axiom to_uint64'def :
 385   forall (x:Numbers.BinNums.Z),
 386   ((x < 0%Z)%Z ->
 387    ((to_uint64 x) = (to_uint64 (x + 18446744073709551616%Z)%Z))) /\
 388   (~ (x < 0%Z)%Z ->
 389    ((18446744073709551616%Z <= x)%Z ->
 390     ((to_uint64 x) = (to_uint64 (x - 18446744073709551616%Z)%Z))) /\
 391    (~ (18446744073709551616%Z <= x)%Z -> ((to_uint64 x) = x))).
 392
 393 Parameter to_sint64: Numbers.BinNums.Z -> Numbers.BinNums.Z.
 394
 395 Axiom to_sint64'def :
 396   forall (x:Numbers.BinNums.Z),
 397   ((x < (-9223372036854775808%Z)%Z)%Z ->
 398    ((to_sint64 x) = (to_sint64 (x + 18446744073709551616%Z)%Z))) /\
 399   (~ (x < (-9223372036854775808%Z)%Z)%Z ->
 400    ((9223372036854775808%Z <= x)%Z ->
 401     ((to_sint64 x) = (to_sint64 (x - 18446744073709551616%Z)%Z))) /\
 402    (~ (9223372036854775808%Z <= x)%Z -> ((to_sint64 x) = x))).
 403
 404 Parameter two_power_abs: Numbers.BinNums.Z -> Numbers.BinNums.Z.
 405
 406 (* Why3 assumption *)
 407 Definition is_uint (n:Numbers.BinNums.Z) (x:Numbers.BinNums.Z) : Prop :=
 408   (0%Z <= x)%Z /\ (x < (two_power_abs n))%Z.
 409
 410 (* Why3 assumption *)
 411 Definition is_sint (n:Numbers.BinNums.Z) (x:Numbers.BinNums.Z) : Prop :=
 412   ((-(two_power_abs n))%Z <= x)%Z /\ (x < (two_power_abs n))%Z.
 413
 414 Parameter to_uint:
 415   Numbers.BinNums.Z -> Numbers.BinNums.Z -> Numbers.BinNums.Z.
 416
 417 Parameter to_sint:
 418   Numbers.BinNums.Z -> Numbers.BinNums.Z -> Numbers.BinNums.Z.
 419
 420 Axiom is_to_uint8 : forall (x:Numbers.BinNums.Z), is_uint8 (to_uint8 x).
 421
 422 Axiom is_to_sint8 : forall (x:Numbers.BinNums.Z), is_sint8 (to_sint8 x).
 423
 424 Axiom is_to_uint16 : forall (x:Numbers.BinNums.Z), is_uint16 (to_uint16 x).
 425
 426 Axiom is_to_sint16 : forall (x:Numbers.BinNums.Z), is_sint16 (to_sint16 x).
 427
 428 Axiom is_to_uint32 : forall (x:Numbers.BinNums.Z), is_uint32 (to_uint32 x).
 429
 430 Axiom is_to_sint32 : forall (x:Numbers.BinNums.Z), is_sint32 (to_sint32 x).
 431
 432 Axiom is_to_uint64 : forall (x:Numbers.BinNums.Z), is_uint64 (to_uint64 x).
 433
 434 Axiom is_to_sint64 : forall (x:Numbers.BinNums.Z), is_sint64 (to_sint64 x).
 435
 436 Axiom id_uint8 :
 437   forall (x:Numbers.BinNums.Z), is_uint8 x -> ((to_uint8 x) = x).
 438
 439 Axiom id_sint8 :
 440   forall (x:Numbers.BinNums.Z), is_sint8 x -> ((to_sint8 x) = x).
 441
 442 Axiom id_uint16 :
 443   forall (x:Numbers.BinNums.Z), is_uint16 x -> ((to_uint16 x) = x).
 444
 445 Axiom id_sint16 :
 446   forall (x:Numbers.BinNums.Z), is_sint16 x -> ((to_sint16 x) = x).
 447
 448 Axiom id_uint32 :
 449   forall (x:Numbers.BinNums.Z), is_uint32 x -> ((to_uint32 x) = x).
 450
 451 Axiom id_sint32 :
 452   forall (x:Numbers.BinNums.Z), is_sint32 x -> ((to_sint32 x) = x).
 453
 454 Axiom id_uint64 :
 455   forall (x:Numbers.BinNums.Z), is_uint64 x -> ((to_uint64 x) = x).
 456
 457 Axiom id_sint64 :
 458   forall (x:Numbers.BinNums.Z), is_sint64 x -> ((to_sint64 x) = x).
 459
 460 Axiom id_uint8_inl :
 461   forall (x:Numbers.BinNums.Z), (0%Z <= x)%Z /\ (x < 256%Z)%Z ->
 462   ((to_uint8 x) = x).
 463
 464 Axiom id_sint8_inl :
 465   forall (x:Numbers.BinNums.Z), ((-128%Z)%Z <= x)%Z /\ (x < 128%Z)%Z ->
 466   ((to_sint8 x) = x).
 467
 468 Axiom id_uint16_inl :
 469   forall (x:Numbers.BinNums.Z), (0%Z <= x)%Z /\ (x < 65536%Z)%Z ->
 470   ((to_uint16 x) = x).
 471
 472 Axiom id_sint16_inl :
 473   forall (x:Numbers.BinNums.Z), ((-32768%Z)%Z <= x)%Z /\ (x < 32768%Z)%Z ->
 474   ((to_sint16 x) = x).
 475
 476 Axiom id_uint32_inl :
 477   forall (x:Numbers.BinNums.Z), (0%Z <= x)%Z /\ (x < 4294967296%Z)%Z ->
 478   ((to_uint32 x) = x).
 479
 480 Axiom id_sint32_inl :
 481   forall (x:Numbers.BinNums.Z),
 482   ((-2147483648%Z)%Z <= x)%Z /\ (x < 2147483648%Z)%Z -> ((to_sint32 x) = x).
 483
 484 Axiom id_uint64_inl :
 485   forall (x:Numbers.BinNums.Z),
 486   (0%Z <= x)%Z /\ (x < 18446744073709551616%Z)%Z -> ((to_uint64 x) = x).
 487
 488 Axiom id_sint64_inl :
 489   forall (x:Numbers.BinNums.Z),
 490   ((-9223372036854775808%Z)%Z <= x)%Z /\ (x < 9223372036854775808%Z)%Z ->
 491   ((to_sint64 x) = x).
 492
 493 Axiom proj_int8 :
 494   forall (x:Numbers.BinNums.Z), ((to_sint8 (to_uint8 x)) = (to_sint8 x)).
 495
 496 Axiom proj_int16 :
 497   forall (x:Numbers.BinNums.Z), ((to_sint16 (to_uint16 x)) = (to_sint16 x)).
 498
 499 Axiom proj_int32 :
 500   forall (x:Numbers.BinNums.Z), ((to_sint32 (to_uint32 x)) = (to_sint32 x)).
 501
 502 Axiom proj_int64 :
 503   forall (x:Numbers.BinNums.Z), ((to_sint64 (to_uint64 x)) = (to_sint64 x)).
 504
 505 (* Why3 assumption *)
 506 Definition P_SomeEqual_1_ (Mint:addr -> Numbers.BinNums.Z) (a:addr)
 507     (m:Numbers.BinNums.Z) (n:Numbers.BinNums.Z) (v:Numbers.BinNums.Z) : Prop :=
 508   exists i:Numbers.BinNums.Z,
 509   (((Mint (shift a i)) = v) /\ (m <= i)%Z) /\ (i < n)%Z.
 510
 511 (* Why3 assumption *)
 512 Definition P_NoneEqual_1_ (Mint:addr -> Numbers.BinNums.Z) (a:addr)
 513     (m:Numbers.BinNums.Z) (n:Numbers.BinNums.Z) (v:Numbers.BinNums.Z) : Prop :=
 514   forall (i:Numbers.BinNums.Z), (m <= i)%Z -> (i < n)%Z ->
 515   ~ ((Mint (shift a i)) = v).
 516
 517 Axiom Q_NotSomeEqual_NoneEqual :
 518   forall (Mint:addr -> Numbers.BinNums.Z) (a:addr) (v:Numbers.BinNums.Z)
 519     (m:Numbers.BinNums.Z) (n:Numbers.BinNums.Z),
 520   is_sint32 v -> ~ P_SomeEqual_1_ Mint a m n v -> P_NoneEqual_1_ Mint a m n v.
 521
 522 Axiom Q_NoneEqual_NotSomeEqual :
 523   forall (Mint:addr -> Numbers.BinNums.Z) (a:addr) (v:Numbers.BinNums.Z)
 524     (m:Numbers.BinNums.Z) (n:Numbers.BinNums.Z),
 525   is_sint32 v -> P_NoneEqual_1_ Mint a m n v -> ~ P_SomeEqual_1_ Mint a m n v.
 526
 527 Parameter L_Find_1_:
 528   (addr -> Numbers.BinNums.Z) -> addr -> Numbers.BinNums.Z ->
 529   Numbers.BinNums.Z -> Numbers.BinNums.Z -> Numbers.BinNums.Z.
 530
 531 Axiom L_Find_1__def :
 532   forall (Mint:addr -> Numbers.BinNums.Z) (a:addr) (m:Numbers.BinNums.Z)
 533     (n:Numbers.BinNums.Z) (v:Numbers.BinNums.Z),
 534   let x := ((-1%Z)%Z + n)%Z in
 535   let x1 := L_Find_1_ Mint a m x v in
 536   let x2 := ((-1%Z)%Z * m)%Z in
 537   ((n <= m)%Z -> ((L_Find_1_ Mint a m n v) = 0%Z)) /\
 538   (~ (n <= m)%Z ->
 539    ((0%Z <= x1)%Z /\ (((2%Z + m)%Z + x1)%Z <= n)%Z ->
 540     ((L_Find_1_ Mint a m n v) = x1)) /\
 541    (~ ((0%Z <= x1)%Z /\ (((2%Z + m)%Z + x1)%Z <= n)%Z) ->
 542     (((Mint (shift a x)) = v) ->
 543      ((L_Find_1_ Mint a m n v) = (((-1%Z)%Z + n)%Z + x2)%Z)) /\
 544     (~ ((Mint (shift a x)) = v) -> ((L_Find_1_ Mint a m n v) = (n + x2)%Z)))).
 545
 546 Axiom Q_Find_ResultNoneEqual :
 547   forall (Mint:addr -> Numbers.BinNums.Z) (a:addr) (v:Numbers.BinNums.Z)
 548     (m:Numbers.BinNums.Z) (n:Numbers.BinNums.Z),
 549   (m <= n)%Z -> is_sint32 v ->
 550   P_NoneEqual_1_ Mint a m (m + (L_Find_1_ Mint a m n v))%Z v.
 551
 552 Axiom Q_Find_SomeEqual :
 553   forall (Mint:addr -> Numbers.BinNums.Z) (a:addr) (v:Numbers.BinNums.Z)
 554     (k:Numbers.BinNums.Z) (m:Numbers.BinNums.Z) (n:Numbers.BinNums.Z),
 555   let x := Mint (shift a k) in
 556   (x = v) -> (m <= k)%Z -> (k < n)%Z -> is_sint32 v -> is_sint32 x ->
 557   P_NoneEqual_1_ Mint a m k v -> ((m + (L_Find_1_ Mint a m n v))%Z = k).
 558
 559 Axiom Q_Find_NoneEqual :
 560   forall (Mint:addr -> Numbers.BinNums.Z) (a:addr) (v:Numbers.BinNums.Z)
 561     (m:Numbers.BinNums.Z) (n:Numbers.BinNums.Z),
 562   (m <= n)%Z -> is_sint32 v -> P_NoneEqual_1_ Mint a m n v ->
 563   ((m + (L_Find_1_ Mint a m n v))%Z = n).
 564
 565 Axiom Q_Find_Limit :
 566   forall (Mint:addr -> Numbers.BinNums.Z) (a:addr) (v:Numbers.BinNums.Z)
 567     (k:Numbers.BinNums.Z) (m:Numbers.BinNums.Z) (n:Numbers.BinNums.Z),
 568   let x := Mint (shift a k) in
 569   (x = v) -> (m <= k)%Z -> (k < n)%Z -> is_sint32 v -> is_sint32 x ->
 570   ((m + (L_Find_1_ Mint a m n v))%Z <= k)%Z.
 571
 572 Axiom Q_Find_Extend :
 573   forall (Mint:addr -> Numbers.BinNums.Z) (a:addr) (v:Numbers.BinNums.Z)
 574     (k:Numbers.BinNums.Z) (m:Numbers.BinNums.Z) (n:Numbers.BinNums.Z),
 575   let x := Mint (shift a k) in
 576   (x = v) -> ((m + (L_Find_1_ Mint a m k v))%Z = k) -> (m <= k)%Z ->
 577   (k < n)%Z -> is_sint32 v -> is_sint32 x ->
 578   ((m + (L_Find_1_ Mint a m n v))%Z = k).
 579
 580 Axiom Q_Find_Increasing :
 581   forall (Mint:addr -> Numbers.BinNums.Z) (a:addr) (v:Numbers.BinNums.Z)
 582     (k:Numbers.BinNums.Z) (m:Numbers.BinNums.Z) (n:Numbers.BinNums.Z),
 583   (m <= k)%Z -> (k <= n)%Z -> is_sint32 v ->
 584   ((L_Find_1_ Mint a m k v) <= (L_Find_1_ Mint a m n v))%Z.
 585
 586 Axiom Q_Find_WeaklyIncreasing :
 587   forall (Mint:addr -> Numbers.BinNums.Z) (a:addr) (v:Numbers.BinNums.Z)
 588     (m:Numbers.BinNums.Z) (n:Numbers.BinNums.Z),
 589   (m <= n)%Z -> is_sint32 v ->
 590   ((L_Find_1_ Mint a m n v) <= (L_Find_1_ Mint a m (1%Z + n)%Z v))%Z.
 591
 592 Axiom Q_Find_Upper :
 593   forall (Mint:addr -> Numbers.BinNums.Z) (a:addr) (v:Numbers.BinNums.Z)
 594     (m:Numbers.BinNums.Z) (n:Numbers.BinNums.Z),
 595   (m <= n)%Z -> is_sint32 v -> ((m + (L_Find_1_ Mint a m n v))%Z <= n)%Z.
 596
 597 Axiom Q_Find_Lower :
 598   forall (Mint:addr -> Numbers.BinNums.Z) (a:addr) (v:Numbers.BinNums.Z)
 599     (m:Numbers.BinNums.Z) (n:Numbers.BinNums.Z),
 600   is_sint32 v -> (0%Z <= (L_Find_1_ Mint a m n v))%Z.
 601
 602 Axiom Q_Find_MissMiss :
 603   forall (Mint:addr -> Numbers.BinNums.Z) (a:addr) (v:Numbers.BinNums.Z)
 604     (m:Numbers.BinNums.Z) (n:Numbers.BinNums.Z),
 605   let x := Mint (shift a n) in
 606   let x1 := (1%Z + n)%Z in
 607   ~ (x = v) -> ((m + (L_Find_1_ Mint a m n v))%Z = n) -> (m <= n)%Z ->
 608   is_sint32 v -> is_sint32 x -> ((m + (L_Find_1_ Mint a m x1 v))%Z = x1).
 609
 610 Axiom Q_Find_MissHit :
 611   forall (Mint:addr -> Numbers.BinNums.Z) (a:addr) (v:Numbers.BinNums.Z)
 612     (m:Numbers.BinNums.Z) (n:Numbers.BinNums.Z),
 613   let x := Mint (shift a n) in
 614   (x = v) -> ((m + (L_Find_1_ Mint a m n v))%Z = n) -> (m <= n)%Z ->
 615   is_sint32 v -> is_sint32 x ->
 616   ((m + (L_Find_1_ Mint a m (1%Z + n)%Z v))%Z = n).
 617
 618 Axiom Q_Find_Hit :
 619   forall (Mint:addr -> Numbers.BinNums.Z) (a:addr) (v:Numbers.BinNums.Z)
 620     (m:Numbers.BinNums.Z) (n:Numbers.BinNums.Z),
 621   let x := L_Find_1_ Mint a m n v in
 622   (m <= n)%Z -> ((m + x)%Z < n)%Z -> is_sint32 v ->
 623   ((L_Find_1_ Mint a m (1%Z + n)%Z v) = x).
 624
 625 Axiom Q_Find_Empty :
 626   forall (Mint:addr -> Numbers.BinNums.Z) (a:addr) (v:Numbers.BinNums.Z)
 627     (m:Numbers.BinNums.Z) (n:Numbers.BinNums.Z),
 628   (n <= m)%Z -> is_sint32 v -> ((L_Find_1_ Mint a m n v) = 0%Z).
 629
 630 (* Why3 goal *)
 631 Theorem wp_goal :
 632   forall (t:addr -> Numbers.BinNums.Z) (a:addr) (i:Numbers.BinNums.Z)
 633     (i1:Numbers.BinNums.Z) (i2:Numbers.BinNums.Z),
 634   let x := L_Find_1_ t a i i1 i2 in
 635   let x1 := (i + x)%Z in
 636   let x2 := t (shift a x1) in
 637   (0%Z <= x)%Z -> (x1 < i1)%Z -> is_sint32 i2 -> is_sint32 x2 -> (x2 = i2).
 638 Proof.
 639 intros t a i i1 i2 x x1 x2 h1 h2 h3 h4.
 640
 641 Qed.
 642