bench/encoding/why2/caduceus/binary_search_why.why

   1 logic eq_unit : unit, unit -> prop
   2
   3 logic neq_unit : unit, unit -> prop
   4
   5 logic eq_bool : bool, bool -> prop
   6
   7 logic neq_bool : bool, bool -> prop
   8
   9 logic lt_int : int, int -> prop
  10
  11 logic le_int : int, int -> prop
  12
  13 logic gt_int : int, int -> prop
  14
  15 logic ge_int : int, int -> prop
  16
  17 logic eq_int : int, int -> prop
  18
  19 logic neq_int : int, int -> prop
  20
  21 logic add_int : int, int -> int
  22
  23 logic sub_int : int, int -> int
  24
  25 logic mul_int : int, int -> int
  26
  27 logic div_int : int, int -> int
  28
  29 logic mod_int : int, int -> int
  30
  31 logic neg_int : int -> int
  32
  33 predicate zwf_zero(a: int, b: int) = ((0 <= b) and (a < b))
  34
  35 logic bw_compl : int -> int
  36
  37 logic bw_and : int, int -> int
  38
  39 logic bw_xor : int, int -> int
  40
  41 logic bw_or : int, int -> int
  42
  43 logic lsl : int, int -> int
  44
  45 logic lsr : int, int -> int
  46
  47 type 'z pointer
  48
  49 type 'z addr
  50
  51 type alloc_table
  52
  53 logic block_length : alloc_table, 'a1 pointer -> int
  54
  55 logic base_addr : 'a1 pointer -> 'a1 addr
  56
  57 logic offset : 'a1 pointer -> int
  58
  59 logic shift : 'a1 pointer, int -> 'a1 pointer
  60
  61 logic sub_pointer : 'a1 pointer, 'a1 pointer -> int
  62
  63 predicate lt_pointer(p1: 'a1 pointer, p2: 'a1 pointer) =
  64   ((base_addr(p1) = base_addr(p2)) and (offset(p1) < offset(p2)))
  65
  66 predicate le_pointer(p1: 'a1 pointer, p2: 'a1 pointer) =
  67   ((base_addr(p1) = base_addr(p2)) and (offset(p1) <= offset(p2)))
  68
  69 predicate gt_pointer(p1: 'a1 pointer, p2: 'a1 pointer) =
  70   ((base_addr(p1) = base_addr(p2)) and (offset(p1) > offset(p2)))
  71
  72 predicate ge_pointer(p1: 'a1 pointer, p2: 'a1 pointer) =
  73   ((base_addr(p1) = base_addr(p2)) and (offset(p1) >= offset(p2)))
  74
  75 predicate valid(a: alloc_table, p: 'a1 pointer) =
  76   ((0 <= offset(p)) and (offset(p) < block_length(a, p)))
  77
  78 predicate valid_index(a: alloc_table, p: 'a1 pointer, i: int) =
  79   ((0 <= (offset(p) + i)) and ((offset(p) + i) < block_length(a, p)))
  80
  81 predicate valid_range(a: alloc_table, p: 'a1 pointer, i: int, j: int) =
  82   ((0 <= (offset(p) + i)) and ((offset(p) + j) < block_length(a, p)))
  83
  84 axiom offset_shift:
  85   (forall p:'a1 pointer.
  86     (forall i:int [offset(shift(p, i))]. (offset(shift(p,
  87       i)) = (offset(p) + i))))
  88
  89 axiom shift_zero: (forall p:'a1 pointer [shift(p, 0)]. (shift(p, 0) = p))
  90
  91 axiom shift_shift:
  92   (forall p:'a1 pointer.
  93     (forall i:int.
  94       (forall j:int [shift(shift(p, i), j)]. (shift(shift(p, i),
  95         j) = shift(p, (i + j))))))
  96
  97 axiom base_addr_shift:
  98   (forall p:'a1 pointer.
  99     (forall i:int [base_addr(shift(p, i))]. (base_addr(shift(p,
 100       i)) = base_addr(p))))
 101
 102 axiom block_length_shift:
 103   (forall a:alloc_table.
 104     (forall p:'a1 pointer.
 105       (forall i:int [block_length(a, shift(p, i))]. (block_length(a, shift(p,
 106         i)) = block_length(a, p)))))
 107
 108 axiom base_addr_block_length:
 109   (forall a:alloc_table.
 110     (forall p1:'a1 pointer.
 111       (forall p2:'a1 pointer.
 112         ((base_addr(p1) = base_addr(p2)) -> (block_length(a,
 113          p1) = block_length(a, p2))))))
 114
 115 axiom pointer_pair_1:
 116   (forall p1:'a1 pointer.
 117     (forall p2:'a1 pointer.
 118       (((base_addr(p1) = base_addr(p2)) and (offset(p1) = offset(p2))) ->
 119        (p1 = p2))))
 120
 121 axiom pointer_pair_2:
 122   (forall p1:'a1 pointer.
 123     (forall p2:'a1 pointer.
 124       ((p1 = p2) ->
 125        ((base_addr(p1) = base_addr(p2)) and (offset(p1) = offset(p2))))))
 126
 127 axiom neq_base_addr_neq_shift:
 128   (forall p1:'a1 pointer.
 129     (forall p2:'a1 pointer.
 130       (forall i:int.
 131         (forall j:int.
 132           ((base_addr(p1) <> base_addr(p2)) -> (shift(p1, i) <> shift(p2, j)))))))
 133
 134 axiom neq_offset_neq_shift:
 135   (forall p1:'a1 pointer.
 136     (forall p2:'a1 pointer.
 137       (forall i:int.
 138         (forall j:int.
 139           (((offset(p1) + i) <> (offset(p2) + j)) -> (shift(p1,
 140            i) <> shift(p2, j)))))))
 141
 142 axiom eq_offset_eq_shift:
 143   (forall p1:'a1 pointer.
 144     (forall p2:'a1 pointer.
 145       (forall i:int.
 146         (forall j:int.
 147           ((base_addr(p1) = base_addr(p2)) ->
 148            (((offset(p1) + i) = (offset(p2) + j)) -> (shift(p1,
 149             i) = shift(p2, j))))))))
 150
 151 axiom valid_index_valid_shift:
 152   (forall a:alloc_table.
 153     (forall p:'a1 pointer.
 154       (forall i:int. (valid_index(a, p, i) -> valid(a, shift(p, i))))))
 155
 156 axiom valid_range_valid_shift:
 157   (forall a:alloc_table.
 158     (forall p:'a1 pointer.
 159       (forall i:int.
 160         (forall j:int.
 161           (forall k:int.
 162             (valid_range(a, p, i, j) ->
 163              (((i <= k) and (k <= j)) -> valid(a, shift(p, k)))))))))
 164
 165 axiom valid_range_valid:
 166   (forall a:alloc_table.
 167     (forall p:'a1 pointer.
 168       (forall i:int.
 169         (forall j:int.
 170           (valid_range(a, p, i, j) ->
 171            (((i <= 0) and (0 <= j)) -> valid(a, p)))))))
 172
 173 axiom valid_range_valid_index:
 174   (forall a:alloc_table.
 175     (forall p:'a1 pointer.
 176       (forall i:int.
 177         (forall j:int.
 178           (forall k:int.
 179             (valid_range(a, p, i, j) ->
 180              (((i <= k) and (k <= j)) -> valid_index(a, p, k))))))))
 181
 182 axiom sub_pointer_def:
 183   (forall p1:'a1 pointer.
 184     (forall p2:'a1 pointer.
 185       ((base_addr(p1) = base_addr(p2)) -> (sub_pointer(p1,
 186        p2) = (offset(p1) - offset(p2))))))
 187
 188 type ('a, 'z) memory
 189
 190 logic acc : ('a1, 'a2) memory, 'a2 pointer -> 'a1
 191
 192 logic upd : ('a1, 'a2) memory, 'a2 pointer, 'a1 -> ('a1, 'a2) memory
 193
 194 axiom acc_upd:
 195   (forall m:('a1, 'a2) memory.
 196     (forall p:'a2 pointer.
 197       (forall a:'a1 [acc(upd(m, p, a), p)]. (acc(upd(m, p, a), p) = a))))
 198
 199 axiom acc_upd_neq:
 200   (forall m:('a1, 'a2) memory.
 201     (forall p1:'a2 pointer.
 202       (forall p2:'a2 pointer.
 203         (forall a:'a1 [acc(upd(m, p1, a), p2)].
 204           ((p1 <> p2) -> (acc(upd(m, p1, a), p2) = acc(m, p2)))))))
 205
 206 axiom false_not_true: (false <> true)
 207
 208 type 'z pset
 209
 210 logic pset_empty : 'a1 pset
 211
 212 logic pset_singleton : 'a1 pointer -> 'a1 pset
 213
 214 logic pset_star : 'a2 pset, ('a1 pointer, 'a2) memory -> 'a1 pset
 215
 216 logic pset_all : 'a1 pset -> 'a1 pset
 217
 218 logic pset_range : 'a1 pset, int, int -> 'a1 pset
 219
 220 logic pset_range_left : 'a1 pset, int -> 'a1 pset
 221
 222 logic pset_range_right : 'a1 pset, int -> 'a1 pset
 223
 224 logic pset_acc_all : 'a2 pset, ('a1 pointer, 'a2) memory -> 'a1 pset
 225
 226 logic pset_acc_range : 'a2 pset, ('a1 pointer, 'a2) memory, int,
 227 int -> 'a1 pset
 228
 229 logic pset_acc_range_left : 'a2 pset, ('a1 pointer, 'a2) memory,
 230 int -> 'a1 pset
 231
 232 logic pset_acc_range_right : 'a2 pset, ('a1 pointer, 'a2) memory,
 233 int -> 'a1 pset
 234
 235 logic pset_union : 'a1 pset, 'a1 pset -> 'a1 pset
 236
 237 logic not_in_pset : 'a1 pointer, 'a1 pset -> prop
 238
 239 predicate not_assigns(a: alloc_table, m1: ('a1, 'a2) memory, m2: ('a1,
 240   'a2) memory, l: 'a2 pset) =
 241   (forall p:'a2 pointer.
 242     (valid(a, p) -> (not_in_pset(p, l) -> (acc(m2, p) = acc(m1, p)))))
 243
 244 axiom pset_empty_intro: (forall p:'a1 pointer. not_in_pset(p, pset_empty))
 245
 246 axiom pset_singleton_intro:
 247   (forall p1:'a1 pointer.
 248     (forall p2:'a1 pointer [not_in_pset(p1, pset_singleton(p2))].
 249       ((p1 <> p2) -> not_in_pset(p1, pset_singleton(p2)))))
 250
 251 axiom pset_singleton_elim:
 252   (forall p1:'a1 pointer.
 253     (forall p2:'a1 pointer [not_in_pset(p1, pset_singleton(p2))].
 254       (not_in_pset(p1, pset_singleton(p2)) -> (p1 <> p2))))
 255
 256 axiom not_not_in_singleton:
 257   (forall p:'a1 pointer. (not not_in_pset(p, pset_singleton(p))))
 258
 259 axiom pset_union_intro:
 260   (forall l1:'a1 pset.
 261     (forall l2:'a1 pset.
 262       (forall p:'a1 pointer [not_in_pset(p, pset_union(l1, l2))].
 263         ((not_in_pset(p, l1) and not_in_pset(p, l2)) -> not_in_pset(p,
 264          pset_union(l1, l2))))))
 265
 266 axiom pset_union_elim1:
 267   (forall l1:'a1 pset.
 268     (forall l2:'a1 pset.
 269       (forall p:'a1 pointer [not_in_pset(p, pset_union(l1, l2))].
 270         (not_in_pset(p, pset_union(l1, l2)) -> not_in_pset(p, l1)))))
 271
 272 axiom pset_union_elim2:
 273   (forall l1:'a1 pset.
 274     (forall l2:'a1 pset.
 275       (forall p:'a1 pointer [not_in_pset(p, pset_union(l1, l2))].
 276         (not_in_pset(p, pset_union(l1, l2)) -> not_in_pset(p, l2)))))
 277
 278 axiom pset_star_intro:
 279   (forall l:'a1 pset.
 280     (forall m:('a2 pointer, 'a1) memory.
 281       (forall p:'a2 pointer [not_in_pset(p, pset_star(l, m))].
 282         ((forall p1:'a1 pointer. ((p = acc(m, p1)) -> not_in_pset(p1, l))) ->
 283          not_in_pset(p, pset_star(l, m))))))
 284
 285 axiom pset_star_elim:
 286   (forall l:'a1 pset.
 287     (forall m:('a2 pointer, 'a1) memory.
 288       (forall p:'a2 pointer [not_in_pset(p, pset_star(l, m))].
 289         (not_in_pset(p, pset_star(l, m)) ->
 290          (forall p1:'a1 pointer. ((p = acc(m, p1)) -> not_in_pset(p1, l)))))))
 291
 292 axiom pset_all_intro:
 293   (forall p:'a1 pointer.
 294     (forall l:'a1 pset [not_in_pset(p, pset_all(l))].
 295       ((forall p1:'a1 pointer.
 296          ((not not_in_pset(p1, l)) -> (base_addr(p) <> base_addr(p1)))) ->
 297        not_in_pset(p, pset_all(l)))))
 298
 299 axiom pset_all_elim:
 300   (forall p:'a1 pointer.
 301     (forall l:'a1 pset [not_in_pset(p, pset_all(l))].
 302       (not_in_pset(p, pset_all(l)) ->
 303        (forall p1:'a1 pointer.
 304          ((not not_in_pset(p1, l)) -> (base_addr(p) <> base_addr(p1)))))))
 305
 306 axiom pset_range_intro:
 307   (forall p:'a1 pointer.
 308     (forall l:'a1 pset.
 309       (forall a:int.
 310         (forall b:int [not_in_pset(p, pset_range(l, a, b))].
 311           ((forall p1:'a1 pointer.
 312              (not_in_pset(p1, l) or
 313               (forall i:int.
 314                 (((a <= i) and (i <= b)) -> (p <> shift(p1, i)))))) ->
 315            not_in_pset(p, pset_range(l, a, b)))))))
 316
 317 axiom pset_range_elim:
 318   (forall p:'a1 pointer.
 319     (forall l:'a1 pset.
 320       (forall a:int.
 321         (forall b:int [not_in_pset(p, pset_range(l, a, b))].
 322           (not_in_pset(p, pset_range(l, a, b)) ->
 323            (forall p1:'a1 pointer.
 324              ((not not_in_pset(p1, l)) ->
 325               (forall i:int.
 326                 (((a <= i) and (i <= b)) -> (shift(p1, i) <> p))))))))))
 327
 328 axiom pset_range_left_intro:
 329   (forall p:'a1 pointer.
 330     (forall l:'a1 pset.
 331       (forall a:int [not_in_pset(p, pset_range_left(l, a))].
 332         ((forall p1:'a1 pointer.
 333            (not_in_pset(p1, l) or
 334             (forall i:int. ((i <= a) -> (p <> shift(p1, i)))))) ->
 335          not_in_pset(p, pset_range_left(l, a))))))
 336
 337 axiom pset_range_left_elim:
 338   (forall p:'a1 pointer.
 339     (forall l:'a1 pset.
 340       (forall a:int [not_in_pset(p, pset_range_left(l, a))].
 341         (not_in_pset(p, pset_range_left(l, a)) ->
 342          (forall p1:'a1 pointer.
 343            ((not not_in_pset(p1, l)) ->
 344             (forall i:int. ((i <= a) -> (shift(p1, i) <> p)))))))))
 345
 346 axiom pset_range_right_intro:
 347   (forall p:'a1 pointer.
 348     (forall l:'a1 pset.
 349       (forall a:int [not_in_pset(p, pset_range_right(l, a))].
 350         ((forall p1:'a1 pointer.
 351            (not_in_pset(p1, l) or
 352             (forall i:int. ((a <= i) -> (p <> shift(p1, i)))))) ->
 353          not_in_pset(p, pset_range_right(l, a))))))
 354
 355 axiom pset_range_right_elim:
 356   (forall p:'a1 pointer.
 357     (forall l:'a1 pset.
 358       (forall a:int [not_in_pset(p, pset_range_right(l, a))].
 359         (not_in_pset(p, pset_range_right(l, a)) ->
 360          (forall p1:'a1 pointer.
 361            ((not not_in_pset(p1, l)) ->
 362             (forall i:int. ((a <= i) -> (shift(p1, i) <> p)))))))))
 363
 364 axiom pset_acc_all_intro:
 365   (forall p:'a1 pointer.
 366     (forall l:'a2 pset.
 367       (forall m:('a1 pointer, 'a2) memory [not_in_pset(p, pset_acc_all(l,
 368         m))].
 369         ((forall p1:'a2 pointer.
 370            ((not not_in_pset(p1, l)) ->
 371             (forall i:int. (p <> acc(m, shift(p1, i)))))) ->
 372          not_in_pset(p, pset_acc_all(l, m))))))
 373
 374 axiom pset_acc_all_elim:
 375   (forall p:'a1 pointer.
 376     (forall l:'a2 pset.
 377       (forall m:('a1 pointer, 'a2) memory [not_in_pset(p, pset_acc_all(l,
 378         m))].
 379         (not_in_pset(p, pset_acc_all(l, m)) ->
 380          (forall p1:'a2 pointer.
 381            ((not not_in_pset(p1, l)) ->
 382             (forall i:int. (acc(m, shift(p1, i)) <> p))))))))
 383
 384 axiom pset_acc_range_intro:
 385   (forall p:'a1 pointer.
 386     (forall l:'a2 pset.
 387       (forall m:('a1 pointer, 'a2) memory.
 388         (forall a:int.
 389           (forall b:int [not_in_pset(p, pset_acc_range(l, m, a, b))].
 390             ((forall p1:'a2 pointer.
 391                ((not not_in_pset(p1, l)) ->
 392                 (forall i:int.
 393                   (((a <= i) and (i <= b)) -> (p <> acc(m, shift(p1, i))))))) ->
 394              not_in_pset(p, pset_acc_range(l, m, a, b))))))))
 395
 396 axiom pset_acc_range_elim:
 397   (forall p:'a1 pointer.
 398     (forall l:'a2 pset.
 399       (forall m:('a1 pointer, 'a2) memory.
 400         (forall a:int.
 401           (forall b:int.
 402             (not_in_pset(p, pset_acc_range(l, m, a, b)) ->
 403              (forall p1:'a2 pointer.
 404                ((not not_in_pset(p1, l)) ->
 405                 (forall i:int.
 406                   (((a <= i) and (i <= b)) -> (acc(m, shift(p1, i)) <> p)))))))))))
 407
 408 axiom pset_acc_range_left_intro:
 409   (forall p:'a1 pointer.
 410     (forall l:'a2 pset.
 411       (forall m:('a1 pointer, 'a2) memory.
 412         (forall a:int [not_in_pset(p, pset_acc_range_left(l, m, a))].
 413           ((forall p1:'a2 pointer.
 414              ((not not_in_pset(p1, l)) ->
 415               (forall i:int. ((i <= a) -> (p <> acc(m, shift(p1, i))))))) ->
 416            not_in_pset(p, pset_acc_range_left(l, m, a)))))))
 417
 418 axiom pset_acc_range_left_elim:
 419   (forall p:'a1 pointer.
 420     (forall l:'a2 pset.
 421       (forall m:('a1 pointer, 'a2) memory.
 422         (forall a:int [not_in_pset(p, pset_acc_range_left(l, m, a))].
 423           (not_in_pset(p, pset_acc_range_left(l, m, a)) ->
 424            (forall p1:'a2 pointer.
 425              ((not not_in_pset(p1, l)) ->
 426               (forall i:int. ((i <= a) -> (acc(m, shift(p1, i)) <> p))))))))))
 427
 428 axiom pset_acc_range_right_intro:
 429   (forall p:'a1 pointer.
 430     (forall l:'a2 pset.
 431       (forall m:('a1 pointer, 'a2) memory.
 432         (forall a:int [not_in_pset(p, pset_acc_range_right(l, m, a))].
 433           ((forall p1:'a2 pointer.
 434              ((not not_in_pset(p1, l)) ->
 435               (forall i:int. ((a <= i) -> (p <> acc(m, shift(p1, i))))))) ->
 436            not_in_pset(p, pset_acc_range_right(l, m, a)))))))
 437
 438 axiom pset_acc_range_right_elim:
 439   (forall p:'a1 pointer.
 440     (forall l:'a2 pset.
 441       (forall m:('a1 pointer, 'a2) memory.
 442         (forall a:int [not_in_pset(p, pset_acc_range_right(l, m, a))].
 443           (not_in_pset(p, pset_acc_range_right(l, m, a)) ->
 444            (forall p1:'a2 pointer.
 445              ((not not_in_pset(p1, l)) ->
 446               (forall i:int. ((a <= i) -> (acc(m, shift(p1, i)) <> p))))))))))
 447
 448 axiom not_assigns_trans:
 449   (forall a:alloc_table.
 450     (forall l:'a1 pset.
 451       (forall m1:('a2, 'a1) memory.
 452         (forall m2:('a2, 'a1) memory.
 453           (forall m3:('a2, 'a1) memory.
 454             (not_assigns(a, m1, m2, l) ->
 455              (not_assigns(a, m2, m3, l) -> not_assigns(a, m1, m3, l))))))))
 456
 457 axiom not_assigns_refl:
 458   (forall a:alloc_table.
 459     (forall l:'a1 pset.
 460       (forall m:('a2, 'a1) memory. not_assigns(a, m, m, l))))
 461
 462 predicate valid_acc(m1: ('a1 pointer, 'a2) memory) =
 463   (forall p:'a2 pointer.
 464     (forall a:alloc_table. (valid(a, p) -> valid(a, acc(m1, p)))))
 465
 466 predicate valid_acc_range(m1: ('a1 pointer, 'a2) memory, size: int) =
 467   (forall p:'a2 pointer.
 468     (forall a:alloc_table.
 469       (valid(a, p) -> valid_range(a, acc(m1, p), 0, (size - 1)))))
 470
 471 axiom valid_acc_range_valid:
 472   (forall m1:('a1 pointer, 'a2) memory.
 473     (forall size:int.
 474       (forall p:'a2 pointer.
 475         (forall a:alloc_table.
 476           (valid_acc_range(m1, size) -> (valid(a, p) -> valid(a, acc(m1, p))))))))
 477
 478 predicate separation1(m1: ('a1 pointer, 'a2) memory, m2: ('a1 pointer,
 479   'a2) memory) =
 480   (forall p:'a2 pointer.
 481     (forall a:alloc_table.
 482       (valid(a, p) -> (base_addr(acc(m1, p)) <> base_addr(acc(m2, p))))))
 483
 484 predicate separation1_range1(m1: ('a1 pointer, 'a2) memory, m2: ('a1 pointer,
 485   'a2) memory, size: int) =
 486   (forall p:'a2 pointer.
 487     (forall a:alloc_table.
 488       (valid(a, p) ->
 489        (forall i1:int.
 490          (forall i2:int.
 491            (((0 <= i1) and (i1 < size)) ->
 492             (((0 <= i2) and (i2 < size)) -> (base_addr(acc(m1, shift(p,
 493              i1))) <> base_addr(acc(m2, shift(p, i2)))))))))))
 494
 495 predicate separation1_range(m: ('a1 pointer, 'a2) memory, size: int) =
 496   (forall p:'a2 pointer.
 497     (forall a:alloc_table.
 498       (valid(a, p) ->
 499        (forall i1:int.
 500          (((0 <= i1) and (i1 < size)) -> (base_addr(acc(m, shift(p,
 501           i1))) <> base_addr(acc(m, p))))))))
 502
 503 predicate separation2(m1: ('a1 pointer, 'a2) memory, m2: ('a1 pointer,
 504   'a2) memory) =
 505   (forall p1:'a2 pointer.
 506     (forall p2:'a2 pointer.
 507       ((p1 <> p2) -> (base_addr(acc(m1, p1)) <> base_addr(acc(m2, p2))))))
 508
 509 predicate separation2_range1(m1: ('a1 pointer, 'a2) memory, m2: ('a1 pointer,
 510   'a2) memory, size: int) =
 511   (forall p:'a2 pointer.
 512     (forall q:'a2 pointer.
 513       (forall a:alloc_table.
 514         (forall i:int.
 515           (((0 <= i) and (i < size)) -> (base_addr(acc(m1, shift(p,
 516            i))) <> base_addr(acc(m2, q))))))))
 517
 518 logic on_heap : alloc_table, 'a1 pointer -> prop
 519
 520 logic on_stack : alloc_table, 'a1 pointer -> prop
 521
 522 logic fresh : alloc_table, 'a1 pointer -> prop
 523
 524 axiom fresh_not_valid:
 525   (forall a:alloc_table.
 526     (forall p:'a1 pointer. (fresh(a, p) -> (not valid(a, p)))))
 527
 528 axiom fresh_not_valid_shift:
 529   (forall a:alloc_table.
 530     (forall p:'a1 pointer.
 531       (fresh(a, p) -> (forall i:int. (not valid(a, shift(p, i)))))))
 532
 533 logic alloc_extends : alloc_table, alloc_table -> prop
 534
 535 axiom alloc_extends_valid:
 536   (forall a1:alloc_table.
 537     (forall a2:alloc_table.
 538       (alloc_extends(a1, a2) ->
 539        (forall q:'a1 pointer. (valid(a1, q) -> valid(a2, q))))))
 540
 541 axiom alloc_extends_valid_index:
 542   (forall a1:alloc_table.
 543     (forall a2:alloc_table.
 544       (alloc_extends(a1, a2) ->
 545        (forall q:'a1 pointer.
 546          (forall i:int. (valid_index(a1, q, i) -> valid_index(a2, q, i)))))))
 547
 548 axiom alloc_extends_valid_range:
 549   (forall a1:alloc_table.
 550     (forall a2:alloc_table.
 551       (alloc_extends(a1, a2) ->
 552        (forall q:'a1 pointer.
 553          (forall i:int.
 554            (forall j:int.
 555              (valid_range(a1, q, i, j) -> valid_range(a2, q, i, j))))))))
 556
 557 axiom alloc_extends_refl: (forall a:alloc_table. alloc_extends(a, a))
 558
 559 axiom alloc_extends_trans:
 560   (forall a1:alloc_table.
 561     (forall a2:alloc_table.
 562       (forall a3:alloc_table [alloc_extends(a1, a2), alloc_extends(a2, a3)].
 563         (alloc_extends(a1, a2) ->
 564          (alloc_extends(a2, a3) -> alloc_extends(a1, a3))))))
 565
 566 logic free_stack : alloc_table, alloc_table, alloc_table -> prop
 567
 568 axiom free_stack_heap:
 569   (forall a1:alloc_table.
 570     (forall a2:alloc_table.
 571       (forall a3:alloc_table.
 572         (free_stack(a1, a2, a3) ->
 573          (forall p:'a1 pointer.
 574            (valid(a2, p) -> (on_heap(a2, p) -> valid(a3, p))))))))
 575
 576 axiom free_stack_stack:
 577   (forall a1:alloc_table.
 578     (forall a2:alloc_table.
 579       (forall a3:alloc_table.
 580         (free_stack(a1, a2, a3) ->
 581          (forall p:'a1 pointer.
 582            (valid(a1, p) -> (on_stack(a1, p) -> valid(a3, p))))))))
 583
 584 logic null : 'a1 pointer
 585
 586 axiom null_not_valid: (forall a:alloc_table. (not valid(a, null)))
 587
 588 type t_0
 589
 590 type t_1
 591
 592 type t_2
 593
 594 axiom mean_1:
 595   ("CADUCEUS_1":
 596   (forall x:int.
 597     (forall y:int.
 598       ((x <= y) -> ((x <= ((x + y) / 2)) and (((x + y) / 2) <= y))))))
 599
 600 goal binary_search_impl_po_1:
 601   forall t:'a1 pointer.
 602   forall n:int.
 603   forall alloc:alloc_table.
 604   forall intM_t_2:(int,
 605   'a1) memory.
 606   ("CADUCEUS_2":
 607   (((n >= 0) and valid_range(alloc, t, 0, (n - 1))) and
 608    (forall k1:int.
 609      (forall k2:int.
 610        ((((0 <= k1) and (k1 <= k2)) and (k2 <= (n - 1))) -> (acc(intM_t_2,
 611         shift(t, k1)) <= acc(intM_t_2, shift(t, k2)))))))) ->
 612   ("CADUCEUS_4": ((n - 1) <= (n - 1)))
 613
 614 goal binary_search_impl_po_2:
 615   forall t:'a1 pointer.
 616   forall n:int.
 617   forall v:int.
 618   forall alloc:alloc_table.
 619   forall intM_t_2:(int,
 620   'a1) memory.
 621   ("CADUCEUS_2":
 622   (((n >= 0) and valid_range(alloc, t, 0, (n - 1))) and
 623    (forall k1:int.
 624      (forall k2:int.
 625        ((((0 <= k1) and (k1 <= k2)) and (k2 <= (n - 1))) -> (acc(intM_t_2,
 626         shift(t, k1)) <= acc(intM_t_2, shift(t, k2)))))))) ->
 627   forall k:int.
 628   ((0 <= k) and (k < n)) ->
 629   (acc(intM_t_2, shift(t, k)) = v) ->
 630   ("CADUCEUS_4": (k <= (n - 1)))
 631
 632 goal binary_search_impl_po_3:
 633   forall t:'a1 pointer.
 634   forall n:int.
 635   forall v:int.
 636   forall alloc:alloc_table.
 637   forall intM_t_2:(int,
 638   'a1) memory.
 639   ("CADUCEUS_2":
 640   (((n >= 0) and valid_range(alloc, t, 0, (n - 1))) and
 641    (forall k1:int.
 642      (forall k2:int.
 643        ((((0 <= k1) and (k1 <= k2)) and (k2 <= (n - 1))) -> (acc(intM_t_2,
 644         shift(t, k1)) <= acc(intM_t_2, shift(t, k2)))))))) ->
 645   forall l:int.
 646   forall u:int.
 647   ("CADUCEUS_4":
 648   (((0 <= l) and (u <= (n - 1))) and
 649    (forall k:int.
 650      (((0 <= k) and (k < n)) ->
 651       ((acc(intM_t_2, shift(t, k)) = v) -> ((l <= k) and (k <= u))))))) ->
 652   (l <= u) ->
 653   (2 <> 0) ->
 654   forall result:int.
 655   (result = ((l + u) / 2)) ->
 656   forall result0:'a1 pointer.
 657   (result0 = shift(t, result)) ->
 658   valid(alloc, result0)
 659
 660 goal binary_search_impl_po_4:
 661   forall t:'a1 pointer.
 662   forall n:int.
 663   forall v:int.
 664   forall alloc:alloc_table.
 665   forall intM_t_2:(int,
 666   'a1) memory.
 667   ("CADUCEUS_2":
 668   (((n >= 0) and valid_range(alloc, t, 0, (n - 1))) and
 669    (forall k1:int.
 670      (forall k2:int.
 671        ((((0 <= k1) and (k1 <= k2)) and (k2 <= (n - 1))) -> (acc(intM_t_2,
 672         shift(t, k1)) <= acc(intM_t_2, shift(t, k2)))))))) ->
 673   forall l:int.
 674   forall u:int.
 675   ("CADUCEUS_4":
 676   (((0 <= l) and (u <= (n - 1))) and
 677    (forall k:int.
 678      (((0 <= k) and (k < n)) ->
 679       ((acc(intM_t_2, shift(t, k)) = v) -> ((l <= k) and (k <= u))))))) ->
 680   (l <= u) ->
 681   (2 <> 0) ->
 682   forall result:int.
 683   (result = ((l + u) / 2)) ->
 684   forall result0:'a1 pointer.
 685   (result0 = shift(t, result)) ->
 686   valid(alloc, result0) ->
 687   forall result1:int.
 688   (result1 = acc(intM_t_2, result0)) ->
 689   (result1 < v) ->
 690   forall l0:int.
 691   (l0 = (result + 1)) ->
 692   ("CADUCEUS_4": (0 <= l0))
 693
 694 goal binary_search_impl_po_5:
 695   forall t:'a1 pointer.
 696   forall n:int.
 697   forall v:int.
 698   forall alloc:alloc_table.
 699   forall intM_t_2:(int,
 700   'a1) memory.
 701   ("CADUCEUS_2":
 702   (((n >= 0) and valid_range(alloc, t, 0, (n - 1))) and
 703    (forall k1:int.
 704      (forall k2:int.
 705        ((((0 <= k1) and (k1 <= k2)) and (k2 <= (n - 1))) -> (acc(intM_t_2,
 706         shift(t, k1)) <= acc(intM_t_2, shift(t, k2)))))))) ->
 707   forall l:int.
 708   forall u:int.
 709   ("CADUCEUS_4":
 710   (((0 <= l) and (u <= (n - 1))) and
 711    (forall k:int.
 712      (((0 <= k) and (k < n)) ->
 713       ((acc(intM_t_2, shift(t, k)) = v) -> ((l <= k) and (k <= u))))))) ->
 714   (l <= u) ->
 715   (2 <> 0) ->
 716   forall result:int.
 717   (result = ((l + u) / 2)) ->
 718   forall result0:'a1 pointer.
 719   (result0 = shift(t, result)) ->
 720   valid(alloc, result0) ->
 721   forall result1:int.
 722   (result1 = acc(intM_t_2, result0)) ->
 723   (result1 < v) ->
 724   forall l0:int.
 725   (l0 = (result + 1)) ->
 726   ("CADUCEUS_4": (u <= (n - 1)))
 727
 728 goal binary_search_impl_po_6:
 729   forall t:'a1 pointer.
 730   forall n:int.
 731   forall v:int.
 732   forall alloc:alloc_table.
 733   forall intM_t_2:(int,
 734   'a1) memory.
 735   ("CADUCEUS_2":
 736   (((n >= 0) and valid_range(alloc, t, 0, (n - 1))) and
 737    (forall k1:int.
 738      (forall k2:int.
 739        ((((0 <= k1) and (k1 <= k2)) and (k2 <= (n - 1))) -> (acc(intM_t_2,
 740         shift(t, k1)) <= acc(intM_t_2, shift(t, k2)))))))) ->
 741   forall l:int.
 742   forall u:int.
 743   ("CADUCEUS_4":
 744   (((0 <= l) and (u <= (n - 1))) and
 745    (forall k:int.
 746      (((0 <= k) and (k < n)) ->
 747       ((acc(intM_t_2, shift(t, k)) = v) -> ((l <= k) and (k <= u))))))) ->
 748   (l <= u) ->
 749   (2 <> 0) ->
 750   forall result:int.
 751   (result = ((l + u) / 2)) ->
 752   forall result0:'a1 pointer.
 753   (result0 = shift(t, result)) ->
 754   valid(alloc, result0) ->
 755   forall result1:int.
 756   (result1 = acc(intM_t_2, result0)) ->
 757   (result1 < v) ->
 758   forall l0:int.
 759   (l0 = (result + 1)) ->
 760   forall k:int.
 761   ((0 <= k) and (k < n)) ->
 762   (acc(intM_t_2, shift(t, k)) = v) ->
 763   ("CADUCEUS_4": (l0 <= k))
 764
 765 goal binary_search_impl_po_7:
 766   forall t:'a1 pointer.
 767   forall n:int.
 768   forall v:int.
 769   forall alloc:alloc_table.
 770   forall intM_t_2:(int,
 771   'a1) memory.
 772   ("CADUCEUS_2":
 773   (((n >= 0) and valid_range(alloc, t, 0, (n - 1))) and
 774    (forall k1:int.
 775      (forall k2:int.
 776        ((((0 <= k1) and (k1 <= k2)) and (k2 <= (n - 1))) -> (acc(intM_t_2,
 777         shift(t, k1)) <= acc(intM_t_2, shift(t, k2)))))))) ->
 778   forall l:int.
 779   forall u:int.
 780   ("CADUCEUS_4":
 781   (((0 <= l) and (u <= (n - 1))) and
 782    (forall k:int.
 783      (((0 <= k) and (k < n)) ->
 784       ((acc(intM_t_2, shift(t, k)) = v) -> ((l <= k) and (k <= u))))))) ->
 785   (l <= u) ->
 786   (2 <> 0) ->
 787   forall result:int.
 788   (result = ((l + u) / 2)) ->
 789   forall result0:'a1 pointer.
 790   (result0 = shift(t, result)) ->
 791   valid(alloc, result0) ->
 792   forall result1:int.
 793   (result1 = acc(intM_t_2, result0)) ->
 794   (result1 < v) ->
 795   forall l0:int.
 796   (l0 = (result + 1)) ->
 797   forall k:int.
 798   ((0 <= k) and (k < n)) ->
 799   (acc(intM_t_2, shift(t, k)) = v) ->
 800   ("CADUCEUS_4": (k <= u))
 801
 802 goal binary_search_impl_po_8:
 803   forall t:'a1 pointer.
 804   forall n:int.
 805   forall v:int.
 806   forall alloc:alloc_table.
 807   forall intM_t_2:(int,
 808   'a1) memory.
 809   ("CADUCEUS_2":
 810   (((n >= 0) and valid_range(alloc, t, 0, (n - 1))) and
 811    (forall k1:int.
 812      (forall k2:int.
 813        ((((0 <= k1) and (k1 <= k2)) and (k2 <= (n - 1))) -> (acc(intM_t_2,
 814         shift(t, k1)) <= acc(intM_t_2, shift(t, k2)))))))) ->
 815   forall l:int.
 816   forall u:int.
 817   ("CADUCEUS_4":
 818   (((0 <= l) and (u <= (n - 1))) and
 819    (forall k:int.
 820      (((0 <= k) and (k < n)) ->
 821       ((acc(intM_t_2, shift(t, k)) = v) -> ((l <= k) and (k <= u))))))) ->
 822   (l <= u) ->
 823   (2 <> 0) ->
 824   forall result:int.
 825   (result = ((l + u) / 2)) ->
 826   forall result0:'a1 pointer.
 827   (result0 = shift(t, result)) ->
 828   valid(alloc, result0) ->
 829   forall result1:int.
 830   (result1 = acc(intM_t_2, result0)) ->
 831   (result1 < v) ->
 832   forall l0:int.
 833   (l0 = (result + 1)) ->
 834   (0 <= ("CADUCEUS_5": (u - l)))
 835
 836 goal binary_search_impl_po_9:
 837   forall t:'a1 pointer.
 838   forall n:int.
 839   forall v:int.
 840   forall alloc:alloc_table.
 841   forall intM_t_2:(int,
 842   'a1) memory.
 843   ("CADUCEUS_2":
 844   (((n >= 0) and valid_range(alloc, t, 0, (n - 1))) and
 845    (forall k1:int.
 846      (forall k2:int.
 847        ((((0 <= k1) and (k1 <= k2)) and (k2 <= (n - 1))) -> (acc(intM_t_2,
 848         shift(t, k1)) <= acc(intM_t_2, shift(t, k2)))))))) ->
 849   forall l:int.
 850   forall u:int.
 851   ("CADUCEUS_4":
 852   (((0 <= l) and (u <= (n - 1))) and
 853    (forall k:int.
 854      (((0 <= k) and (k < n)) ->
 855       ((acc(intM_t_2, shift(t, k)) = v) -> ((l <= k) and (k <= u))))))) ->
 856   (l <= u) ->
 857   (2 <> 0) ->
 858   forall result:int.
 859   (result = ((l + u) / 2)) ->
 860   forall result0:'a1 pointer.
 861   (result0 = shift(t, result)) ->
 862   valid(alloc, result0) ->
 863   forall result1:int.
 864   (result1 = acc(intM_t_2, result0)) ->
 865   (result1 < v) ->
 866   forall l0:int.
 867   (l0 = (result + 1)) ->
 868   (("CADUCEUS_5": (u - l0)) < ("CADUCEUS_5": (u - l)))
 869
 870 goal binary_search_impl_po_10:
 871   forall t:'a1 pointer.
 872   forall n:int.
 873   forall v:int.
 874   forall alloc:alloc_table.
 875   forall intM_t_2:(int,
 876   'a1) memory.
 877   ("CADUCEUS_2":
 878   (((n >= 0) and valid_range(alloc, t, 0, (n - 1))) and
 879    (forall k1:int.
 880      (forall k2:int.
 881        ((((0 <= k1) and (k1 <= k2)) and (k2 <= (n - 1))) -> (acc(intM_t_2,
 882         shift(t, k1)) <= acc(intM_t_2, shift(t, k2)))))))) ->
 883   forall l:int.
 884   forall u:int.
 885   ("CADUCEUS_4":
 886   (((0 <= l) and (u <= (n - 1))) and
 887    (forall k:int.
 888      (((0 <= k) and (k < n)) ->
 889       ((acc(intM_t_2, shift(t, k)) = v) -> ((l <= k) and (k <= u))))))) ->
 890   (l <= u) ->
 891   (2 <> 0) ->
 892   forall result:int.
 893   (result = ((l + u) / 2)) ->
 894   forall result0:'a1 pointer.
 895   (result0 = shift(t, result)) ->
 896   valid(alloc, result0) ->
 897   forall result1:int.
 898   (result1 = acc(intM_t_2, result0)) ->
 899   (result1 >= v) ->
 900   forall result2:'a1 pointer.
 901   (result2 = shift(t, result)) ->
 902   valid(alloc, result2)
 903
 904 goal binary_search_impl_po_11:
 905   forall t:'a1 pointer.
 906   forall n:int.
 907   forall v:int.
 908   forall alloc:alloc_table.
 909   forall intM_t_2:(int,
 910   'a1) memory.
 911   ("CADUCEUS_2":
 912   (((n >= 0) and valid_range(alloc, t, 0, (n - 1))) and
 913    (forall k1:int.
 914      (forall k2:int.
 915        ((((0 <= k1) and (k1 <= k2)) and (k2 <= (n - 1))) -> (acc(intM_t_2,
 916         shift(t, k1)) <= acc(intM_t_2, shift(t, k2)))))))) ->
 917   forall l:int.
 918   forall u:int.
 919   ("CADUCEUS_4":
 920   (((0 <= l) and (u <= (n - 1))) and
 921    (forall k:int.
 922      (((0 <= k) and (k < n)) ->
 923       ((acc(intM_t_2, shift(t, k)) = v) -> ((l <= k) and (k <= u))))))) ->
 924   (l <= u) ->
 925   (2 <> 0) ->
 926   forall result:int.
 927   (result = ((l + u) / 2)) ->
 928   forall result0:'a1 pointer.
 929   (result0 = shift(t, result)) ->
 930   valid(alloc, result0) ->
 931   forall result1:int.
 932   (result1 = acc(intM_t_2, result0)) ->
 933   (result1 >= v) ->
 934   forall result2:'a1 pointer.
 935   (result2 = shift(t, result)) ->
 936   valid(alloc, result2) ->
 937   forall result3:int.
 938   (result3 = acc(intM_t_2, result2)) ->
 939   (result3 > v) ->
 940   forall u0:int.
 941   (u0 = (result - 1)) ->
 942   ("CADUCEUS_4": (0 <= l))
 943
 944 goal binary_search_impl_po_12:
 945   forall t:'a1 pointer.
 946   forall n:int.
 947   forall v:int.
 948   forall alloc:alloc_table.
 949   forall intM_t_2:(int,
 950   'a1) memory.
 951   ("CADUCEUS_2":
 952   (((n >= 0) and valid_range(alloc, t, 0, (n - 1))) and
 953    (forall k1:int.
 954      (forall k2:int.
 955        ((((0 <= k1) and (k1 <= k2)) and (k2 <= (n - 1))) -> (acc(intM_t_2,
 956         shift(t, k1)) <= acc(intM_t_2, shift(t, k2)))))))) ->
 957   forall l:int.
 958   forall u:int.
 959   ("CADUCEUS_4":
 960   (((0 <= l) and (u <= (n - 1))) and
 961    (forall k:int.
 962      (((0 <= k) and (k < n)) ->
 963       ((acc(intM_t_2, shift(t, k)) = v) -> ((l <= k) and (k <= u))))))) ->
 964   (l <= u) ->
 965   (2 <> 0) ->
 966   forall result:int.
 967   (result = ((l + u) / 2)) ->
 968   forall result0:'a1 pointer.
 969   (result0 = shift(t, result)) ->
 970   valid(alloc, result0) ->
 971   forall result1:int.
 972   (result1 = acc(intM_t_2, result0)) ->
 973   (result1 >= v) ->
 974   forall result2:'a1 pointer.
 975   (result2 = shift(t, result)) ->
 976   valid(alloc, result2) ->
 977   forall result3:int.
 978   (result3 = acc(intM_t_2, result2)) ->
 979   (result3 > v) ->
 980   forall u0:int.
 981   (u0 = (result - 1)) ->
 982   ("CADUCEUS_4": (u0 <= (n - 1)))
 983
 984 goal binary_search_impl_po_13:
 985   forall t:'a1 pointer.
 986   forall n:int.
 987   forall v:int.
 988   forall alloc:alloc_table.
 989   forall intM_t_2:(int,
 990   'a1) memory.
 991   ("CADUCEUS_2":
 992   (((n >= 0) and valid_range(alloc, t, 0, (n - 1))) and
 993    (forall k1:int.
 994      (forall k2:int.
 995        ((((0 <= k1) and (k1 <= k2)) and (k2 <= (n - 1))) -> (acc(intM_t_2,
 996         shift(t, k1)) <= acc(intM_t_2, shift(t, k2)))))))) ->
 997   forall l:int.
 998   forall u:int.
 999   ("CADUCEUS_4":
1000   (((0 <= l) and (u <= (n - 1))) and
1001    (forall k:int.
1002      (((0 <= k) and (k < n)) ->
1003       ((acc(intM_t_2, shift(t, k)) = v) -> ((l <= k) and (k <= u))))))) ->
1004   (l <= u) ->
1005   (2 <> 0) ->
1006   forall result:int.
1007   (result = ((l + u) / 2)) ->
1008   forall result0:'a1 pointer.
1009   (result0 = shift(t, result)) ->
1010   valid(alloc, result0) ->
1011   forall result1:int.
1012   (result1 = acc(intM_t_2, result0)) ->
1013   (result1 >= v) ->
1014   forall result2:'a1 pointer.
1015   (result2 = shift(t, result)) ->
1016   valid(alloc, result2) ->
1017   forall result3:int.
1018   (result3 = acc(intM_t_2, result2)) ->
1019   (result3 > v) ->
1020   forall u0:int.
1021   (u0 = (result - 1)) ->
1022   forall k:int.
1023   ((0 <= k) and (k < n)) ->
1024   (acc(intM_t_2, shift(t, k)) = v) ->
1025   ("CADUCEUS_4": (l <= k))
1026
1027 goal binary_search_impl_po_14:
1028   forall t:'a1 pointer.
1029   forall n:int.
1030   forall v:int.
1031   forall alloc:alloc_table.
1032   forall intM_t_2:(int,
1033   'a1) memory.
1034   ("CADUCEUS_2":
1035   (((n >= 0) and valid_range(alloc, t, 0, (n - 1))) and
1036    (forall k1:int.
1037      (forall k2:int.
1038        ((((0 <= k1) and (k1 <= k2)) and (k2 <= (n - 1))) -> (acc(intM_t_2,
1039         shift(t, k1)) <= acc(intM_t_2, shift(t, k2)))))))) ->
1040   forall l:int.
1041   forall u:int.
1042   ("CADUCEUS_4":
1043   (((0 <= l) and (u <= (n - 1))) and
1044    (forall k:int.
1045      (((0 <= k) and (k < n)) ->
1046       ((acc(intM_t_2, shift(t, k)) = v) -> ((l <= k) and (k <= u))))))) ->
1047   (l <= u) ->
1048   (2 <> 0) ->
1049   forall result:int.
1050   (result = ((l + u) / 2)) ->
1051   forall result0:'a1 pointer.
1052   (result0 = shift(t, result)) ->
1053   valid(alloc, result0) ->
1054   forall result1:int.
1055   (result1 = acc(intM_t_2, result0)) ->
1056   (result1 >= v) ->
1057   forall result2:'a1 pointer.
1058   (result2 = shift(t, result)) ->
1059   valid(alloc, result2) ->
1060   forall result3:int.
1061   (result3 = acc(intM_t_2, result2)) ->
1062   (result3 > v) ->
1063   forall u0:int.
1064   (u0 = (result - 1)) ->
1065   forall k:int.
1066   ((0 <= k) and (k < n)) ->
1067   (acc(intM_t_2, shift(t, k)) = v) ->
1068   ("CADUCEUS_4": (k <= u0))
1069
1070 goal binary_search_impl_po_15:
1071   forall t:'a1 pointer.
1072   forall n:int.
1073   forall v:int.
1074   forall alloc:alloc_table.
1075   forall intM_t_2:(int,
1076   'a1) memory.
1077   ("CADUCEUS_2":
1078   (((n >= 0) and valid_range(alloc, t, 0, (n - 1))) and
1079    (forall k1:int.
1080      (forall k2:int.
1081        ((((0 <= k1) and (k1 <= k2)) and (k2 <= (n - 1))) -> (acc(intM_t_2,
1082         shift(t, k1)) <= acc(intM_t_2, shift(t, k2)))))))) ->
1083   forall l:int.
1084   forall u:int.
1085   ("CADUCEUS_4":
1086   (((0 <= l) and (u <= (n - 1))) and
1087    (forall k:int.
1088      (((0 <= k) and (k < n)) ->
1089       ((acc(intM_t_2, shift(t, k)) = v) -> ((l <= k) and (k <= u))))))) ->
1090   (l <= u) ->
1091   (2 <> 0) ->
1092   forall result:int.
1093   (result = ((l + u) / 2)) ->
1094   forall result0:'a1 pointer.
1095   (result0 = shift(t, result)) ->
1096   valid(alloc, result0) ->
1097   forall result1:int.
1098   (result1 = acc(intM_t_2, result0)) ->
1099   (result1 >= v) ->
1100   forall result2:'a1 pointer.
1101   (result2 = shift(t, result)) ->
1102   valid(alloc, result2) ->
1103   forall result3:int.
1104   (result3 = acc(intM_t_2, result2)) ->
1105   (result3 > v) ->
1106   forall u0:int.
1107   (u0 = (result - 1)) ->
1108   (0 <= ("CADUCEUS_5": (u - l)))
1109
1110 goal binary_search_impl_po_16:
1111   forall t:'a1 pointer.
1112   forall n:int.
1113   forall v:int.
1114   forall alloc:alloc_table.
1115   forall intM_t_2:(int,
1116   'a1) memory.
1117   ("CADUCEUS_2":
1118   (((n >= 0) and valid_range(alloc, t, 0, (n - 1))) and
1119    (forall k1:int.
1120      (forall k2:int.
1121        ((((0 <= k1) and (k1 <= k2)) and (k2 <= (n - 1))) -> (acc(intM_t_2,
1122         shift(t, k1)) <= acc(intM_t_2, shift(t, k2)))))))) ->
1123   forall l:int.
1124   forall u:int.
1125   ("CADUCEUS_4":
1126   (((0 <= l) and (u <= (n - 1))) and
1127    (forall k:int.
1128      (((0 <= k) and (k < n)) ->
1129       ((acc(intM_t_2, shift(t, k)) = v) -> ((l <= k) and (k <= u))))))) ->
1130   (l <= u) ->
1131   (2 <> 0) ->
1132   forall result:int.
1133   (result = ((l + u) / 2)) ->
1134   forall result0:'a1 pointer.
1135   (result0 = shift(t, result)) ->
1136   valid(alloc, result0) ->
1137   forall result1:int.
1138   (result1 = acc(intM_t_2, result0)) ->
1139   (result1 >= v) ->
1140   forall result2:'a1 pointer.
1141   (result2 = shift(t, result)) ->
1142   valid(alloc, result2) ->
1143   forall result3:int.
1144   (result3 = acc(intM_t_2, result2)) ->
1145   (result3 > v) ->
1146   forall u0:int.
1147   (u0 = (result - 1)) ->
1148   (("CADUCEUS_5": (u0 - l)) < ("CADUCEUS_5": (u - l)))
1149
1150 goal binary_search_impl_po_17:
1151   forall t:'a1 pointer.
1152   forall n:int.
1153   forall v:int.
1154   forall alloc:alloc_table.
1155   forall intM_t_2:(int,
1156   'a1) memory.
1157   ("CADUCEUS_2":
1158   (((n >= 0) and valid_range(alloc, t, 0, (n - 1))) and
1159    (forall k1:int.
1160      (forall k2:int.
1161        ((((0 <= k1) and (k1 <= k2)) and (k2 <= (n - 1))) -> (acc(intM_t_2,
1162         shift(t, k1)) <= acc(intM_t_2, shift(t, k2)))))))) ->
1163   forall l:int.
1164   forall u:int.
1165   ("CADUCEUS_4":
1166   (((0 <= l) and (u <= (n - 1))) and
1167    (forall k:int.
1168      (((0 <= k) and (k < n)) ->
1169       ((acc(intM_t_2, shift(t, k)) = v) -> ((l <= k) and (k <= u))))))) ->
1170   (l <= u) ->
1171   (2 <> 0) ->
1172   forall result:int.
1173   (result = ((l + u) / 2)) ->
1174   forall result0:'a1 pointer.
1175   (result0 = shift(t, result)) ->
1176   valid(alloc, result0) ->
1177   forall result1:int.
1178   (result1 = acc(intM_t_2, result0)) ->
1179   (result1 >= v) ->
1180   forall result2:'a1 pointer.
1181   (result2 = shift(t, result)) ->
1182   valid(alloc, result2) ->
1183   forall result3:int.
1184   (result3 = acc(intM_t_2, result2)) ->
1185   (result3 <= v) ->
1186   ("CADUCEUS_3":
1187   (((result >= 0) and (acc(intM_t_2, shift(t, result)) = v)) or
1188    ((result = (-1)) and
1189     (forall k:int.
1190       (((0 <= k) and (k < n)) -> (acc(intM_t_2, shift(t, k)) <> v))))))
1191
1192 goal binary_search_impl_po_18:
1193   forall t:'a1 pointer.
1194   forall n:int.
1195   forall v:int.
1196   forall alloc:alloc_table.
1197   forall intM_t_2:(int,
1198   'a1) memory.
1199   ("CADUCEUS_2":
1200   (((n >= 0) and valid_range(alloc, t, 0, (n - 1))) and
1201    (forall k1:int.
1202      (forall k2:int.
1203        ((((0 <= k1) and (k1 <= k2)) and (k2 <= (n - 1))) -> (acc(intM_t_2,
1204         shift(t, k1)) <= acc(intM_t_2, shift(t, k2)))))))) ->
1205   forall l:int.
1206   forall u:int.
1207   ("CADUCEUS_4":
1208   (((0 <= l) and (u <= (n - 1))) and
1209    (forall k:int.
1210      (((0 <= k) and (k < n)) ->
1211       ((acc(intM_t_2, shift(t, k)) = v) -> ((l <= k) and (k <= u))))))) ->
1212   (l > u) ->
1213   ("CADUCEUS_3":
1214   ((((-1) >= 0) and (acc(intM_t_2, shift(t, (-1))) = v)) or
1215    (((-1) = (-1)) and
1216     (forall k:int.
1217       (((0 <= k) and (k < n)) -> (acc(intM_t_2, shift(t, k)) <> v))))))
1218